Finite cells and block thresholds

This file constructs the geometric thresholds and the finite families of cells used in Dudley's shared-uniform construction. Weak convergence gives strictly increasing time thresholds after which all cells in the corresponding finite family have the required one-sided mass bound. See Dudley, "Distances of probability measures and random variables" (1968), and Real Analysis and Probability (2002), Theorem 11.7.2.

noncomputable def BGW.Probability.blockThreshold (k : ℕ) : ↑unitInterval

The lower threshold on the common-branch probability at level k.

Equations

• BGW.Probability.blockThreshold k = ⟨1 - 2⁻¹ ^ k, ⋯⟩

noncomputable def BGW.Probability.blockFactor (k : ℕ) : ENNReal

The same threshold as an extended nonnegative real.

Equations

• BGW.Probability.blockFactor k = ENNReal.ofReal ↑(BGW.Probability.blockThreshold k)

theorem BGW.Probability.volume_Ici_blockThreshold (k : ℕ) : MeasureTheory.volume (Set.Ici (blockThreshold k)) = 2⁻¹ ^ k

The volume above the level-k threshold is exactly 2 ^ (-k).

theorem BGW.Probability.le_cellStayProbability_of_mul_le {S : Type u_1} [MeasurableSpace S] {μ ν : MeasureTheory.Measure S} [MeasureTheory.IsProbabilityMeasure ν] {A : ℕ → Set S} {i : ℕ} {t : ↑unitInterval} (hi : ν (A i) ≠ 0) (h : ENNReal.ofReal ↑t * ν (A i) ≤ μ (A i)) : t ≤ cellStayProbability μ ν A i

A one-sided cell-mass bound implies the corresponding lower bound on the common-branch probability.

theorem BGW.Probability.exists_finite_cell_union {S : Type u_1} [MeasurableSpace S] (ν : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure ν] {A : ℕ → Set S} (hmeas : ∀ (i : ℕ), MeasurableSet (A i)) (hdisj : Pairwise (Function.onFun Disjoint A)) (hcover : ⋃ (i : ℕ), A i = Set.univ) (k : ℕ) : ∃ (M : ℕ), 1 - 2⁻¹ ^ k ≤ ν (⋃ i ∈ Finset.range M, A i)

Finite initial segments of a countable probability partition eventually carry at least 1 - 2 ^ (-k) of the mass.

theorem BGW.Probability.exists_strictMono_block_thresholds {S : Type u_1} [PseudoMetricSpace S] [MeasurableSpace S] [BorelSpace S] {P : ℕ → MeasureTheory.ProbabilityMeasure S} {Q : MeasureTheory.ProbabilityMeasure S} (h : Filter.Tendsto P Filter.atTop (nhds Q)) {A : ℕ → ℕ → Set S} (hnull : ∀ (k i : ℕ), ↑Q (frontier (A k i)) = 0) (M : ℕ → ℕ) : ∃ (N : ℕ → ℕ), StrictMono N ∧ (∀ (k : ℕ), k ≤ N k) ∧ ∀ (k n : ℕ), N k ≤ n → ∀ i ∈ Finset.range (M k), blockFactor k * ↑Q (A k i) ≤ ↑(P n) (A k i)

Weak convergence provides strictly increasing block thresholds with one-sided mass bounds on all cells in prescribed finite families.