Oscillation observables for the discrete forest height

The height is interpolated before rescaling. Its modulus is measurable as a lower semicontinuous functional of the continuous height path. The final adjacent height jump is bounded by the modulus on the longer horizon T + 1, and the modulus is monotone in its time scale. A generic dominated convergence lemma for events that eventually fail almost surely is also recorded here.

noncomputable def BGW.StableTrees.HeightTightness.heightOscillation (B : ℕ → ℝ) (n : ℕ) (T δ : ℝ) (ω : ℕ → ℕ) : ℝ

The modulus of continuity at scale δ of the normalized interpolated height on [0,T].

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGW.StableTrees.HeightTightness.maxHeightJump (B : ℕ → ℝ) (n : ℕ) (T : ℝ) (ω : ℕ → ℕ) : ℝ

The normalized largest adjacent height jump before index ⌊n T⌋ + 1.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.HeightTightness.tendsto_measureReal_zero_of_eventually_notMem {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {E : ℕ → Set Ω} (hm : ∀ (N : ℕ), MeasurableSet (E N)) (hev : ∀ᵐ (f : Ω) ∂P, ∀ᶠ (N : ℕ) in Filter.atTop, f ∉ E N) : Filter.Tendsto (fun (N : ℕ) => P.real (E N)) Filter.atTop (nhds 0)

Events that almost surely hold only finitely often have probabilities tending to zero.

theorem BGW.StableTrees.HeightTightness.measurable_heightOscillation (B : ℕ → ℝ) (n : ℕ) (T δ : ℝ) : Measurable (heightOscillation B n T δ)

The interpolated-height modulus is a measurable observable of the offspring sequence.

theorem BGW.StableTrees.HeightTightness.heightDifference_le_heightOscillation (B : ℕ → ℝ) (n : ℕ) {T δ : ℝ} (hT : 0 ≤ T) (ω : ℕ → ℕ) (s t : ↑(Set.Icc 0 T)) (hst : |↑s - ↑t| ≤ δ) : |B n / ↑n * DiscreteForest.forestHeightLin ω (↑n * ↑s) - B n / ↑n * DiscreteForest.forestHeightLin ω (↑n * ↑t)| ≤ heightOscillation B n T δ ω

A pair of height evaluations within distance δ is bounded by the modulus.

theorem BGW.StableTrees.HeightTightness.maxHeightJump_le_heightOscillation (B : ℕ → ℝ) {n : ℕ} (hn : 1 ≤ n) {T : ℝ} (hT : 0 ≤ T) (hB : 0 ≤ B n) (ω : ℕ → ℕ) : maxHeightJump B n T ω ≤ heightOscillation B n (T + 1) (1 / ↑n) ω

The final adjacent jump is controlled by the modulus on the longer horizon T + 1.

theorem BGW.StableTrees.HeightTightness.heightOscillation_le (B : ℕ → ℝ) (n : ℕ) {T δ M : ℝ} (hT : 0 ≤ T) (hM : 0 ≤ M) (ω : ℕ → ℕ) (hb : ∀ (s t : ↑(Set.Icc 0 T)), |↑s - ↑t| ≤ δ → |B n / ↑n * DiscreteForest.forestHeightLin ω (↑n * ↑s) - B n / ↑n * DiscreteForest.forestHeightLin ω (↑n * ↑t)| ≤ M) : heightOscillation B n T δ ω ≤ M

Pairwise bounds on the admissible time pairs bound the entire height modulus.

theorem BGW.StableTrees.HeightTightness.heightOscillation_mono (B : ℕ → ℝ) (n : ℕ) {T δ δ' : ℝ} (hT : 0 ≤ T) (hδ' : 0 ≤ δ') (hδ : δ ≤ δ') (ω : ℕ → ℕ) : heightOscillation B n T δ ω ≤ heightOscillation B n T δ' ω

The height modulus increases with its time scale, for a nonnegative upper scale.