Documentation

BGW.StableTrees.HeightBridgesSequenceHelpers

Extraction and inheritance on the separate height laws #

Each age window retains its own measure. Fubini converts the extracted product limits to almost-everywhere age statements; stable fiber limits are identified using H02 uniqueness.

source
noncomputable def BGW.StableTrees.heightBaseEps (n : ℕ) :
ℝ

The initial cutoff sequence from which universal height cutoffs are extracted.

Equations
Instances For
    source
    theorem BGW.StableTrees.heightBaseEps_pos (n : ℕ) :
    0 < heightBaseEps n

    Initial cutoff positivity.

    source
    theorem BGW.StableTrees.strictAnti_heightBaseEps :
    StrictAnti heightBaseEps

    The initial cutoffs strictly decrease.

    source
    theorem BGW.StableTrees.tendsto_heightBaseEps :
    Filter.Tendsto heightBaseEps Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

    The initial cutoffs tend to zero through positive values.

    source
    theorem BGW.StableTrees.ae_tendsto_comp_of_eventual_subseq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {u : ℕ → Ω → ℝ} {L : Ω → ℝ} {φ ψ : ℕ → ℕ} (hφ : StrictMono φ) (hψ : StrictMono ψ) (hsub : ∃ (N : ℕ), ∀ k ≥ N, ∃ (j : ℕ), ψ k = φ j) (h : ∀ᵐ (x : Ω) ∂μ, Filter.Tendsto (fun (k : ℕ) => u (φ k) x) Filter.atTop (nhds (L x))) :
    ∀ᵐ (x : Ω) ∂μ, Filter.Tendsto (fun (k : ℕ) => u (ψ k) x) Filter.atTop (nhds (L x))

    Fixed almost sure limits are inherited by eventual subsequences.

    source
    theorem BGW.StableTrees.ae_exists_tendsto_comp_of_eventual_subseq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {u : ℕ → Ω → ℝ} {φ ψ : ℕ → ℕ} (hφ : StrictMono φ) (hψ : StrictMono ψ) (hsub : ∃ (N : ℕ), ∀ k ≥ N, ∃ (j : ℕ), ψ k = φ j) (h : ∀ᵐ (x : Ω) ∂μ, ∃ (L : ℝ), Filter.Tendsto (fun (k : ℕ) => u (φ k) x) Filter.atTop (nhds L)) :
    ∀ᵐ (x : Ω) ∂μ, ∃ (L : ℝ), Filter.Tendsto (fun (k : ℕ) => u (ψ k) x) Filter.atTop (nhds L)

    Existence of almost sure finite limits is inherited by eventual subsequences.

    source
    theorem BGW.StableTrees.exists_height_stable_age_subseq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (S : NNReal) (φ : ℕ → ℕ) (hφ : StrictMono φ) :
    ∃ (ψ : ℕ → ℕ), StrictMono ψ ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 ↑S), ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Filter.Tendsto (fun (k : ℕ) => heightApprox (heightBaseEps (φ (ψ k))) f s.toNNReal) Filter.atTop (nhds (height θ f s.toNNReal))

    Extraction at almost every age under the stable law, with H02's identified limit.

    source
    theorem BGW.StableTrees.exists_height_excursion_age_subseq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (S : NNReal) (φ : ℕ → ℕ) (hφ : StrictMono φ) :
    ∃ (ψ : ℕ → ℕ), StrictMono ψ ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 ↑S), ∀ᵐ (e : Excursion) ∂(excursionMeasure θ).restrict {e : Excursion | s.toNNReal < e.lifetime}, ∃ (L : ℝ), Filter.Tendsto (fun (k : ℕ) => heightApprox (heightBaseEps (φ (ψ k))) e.path s.toNNReal) Filter.atTop (nhds L)

    Extraction on a surviving excursion age window, with its own restricted product law.

    source
    theorem BGW.StableTrees.exists_height_unit_age_subseq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (φ : ℕ → ℕ) (hφ : StrictMono φ) :
    ∃ (ψ : ℕ → ℕ), StrictMono ψ ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 1), ∀ᵐ (e : Excursion) ∂↑(unitExcursionLaw θ), ∃ (L : ℝ), Filter.Tendsto (fun (k : ℕ) => heightApprox (heightBaseEps (φ (ψ k))) e.path s.toNNReal) Filter.atTop (nhds L)

    Extraction on the unit-law age window, with its own finite product law.