Adapters for paper contour conventions

The library contour uses duration 2(ζ - 1), while the paper uses duration 2ζ and sets the contour to zero after its tree has been explored. This module proves the time-change and law-transfer bounds between these conventions, measurability for random finite trees, and the divisor estimates from Remark 5.10.

The paper convention is that of I. Kortchemski, Invariance principles for Galton–Watson trees conditioned on the number of leaves (arXiv:1110.2163), with the contour C_{2ζ s}; see also J.-F. Le Gall, Random trees and applications (2005), §1. These adapters serve item C38 of CLASSICAL_THEORY_INPUTS.md.

noncomputable def BGW.PlaneTree.paperTimeChange (t : PlaneTree) : C(↑unitInterval, ↑unitInterval)

The time change s ↦ min 1 (s ζ/(ζ-1)) turning the library's time scale 2(ζ-1) into the paper's 2ζ (for the singleton tree the factor is 0, harmless since the contour is 0).

Equations

• t.paperTimeChange = { toFun := fun (s : ↑unitInterval) => Set.projIcc 0 1 BGW.PlaneTree.paperTimeChange._proof_2 (↑s * (↑t.size / ↑(t.size - 1))), continuous_toFun := ⋯ }

noncomputable def BGW.PlaneTree.paperContourFunction (t : PlaneTree) : C(↑unitInterval, ℝ)

The contour in the paper's time convention, s ↦ C_{2ζ s}.

Equations

• t.paperContourFunction = t.contourFunction.comp t.paperTimeChange

theorem BGW.PlaneTree.abs_paperTimeChange_sub_le (t : PlaneTree) (s : ↑unitInterval) : |↑(t.paperTimeChange s) - ↑s| ≤ 1 / ↑t.size

The time change moves points by at most 1/ζ.

theorem BGW.PlaneTree.paperContourFunction_eq_zero (t : PlaneTree) (s : ↑unitInterval) (hs : ↑(t.size - 1) / ↑t.size ≤ ↑s) : t.paperContourFunction s = 0

The paper contour vanishes on the last 1/ζ of the time interval.

theorem BGW.PlaneTree.norm_paperContourFunction_sub_le (t : PlaneTree) (b ε : ℝ) (hosc : ∀ (s s' : ↑unitInterval), |↑s - ↑s'| ≤ 1 / ↑t.size → |(b⁻¹ • t.contourFunction) s - (b⁻¹ • t.contourFunction) s'| ≤ ε) : ‖b⁻¹ • t.paperContourFunction - b⁻¹ • t.contourFunction‖ ≤ ε

Deterministic uniform bound: if the divided library contour has oscillation ≤ ε at scale 1/ζ, the two conventions are ε-close after division by b.

theorem BGW.PlaneTree.exists_size_bound_norm_paper_sub_le (K : Set C(↑unitInterval, ℝ)) (hK : IsCompact K) {ε : ℝ} (hε : 0 < ε) : ∃ (R : ℝ), ∀ (t : PlaneTree) (b : ℝ), R ≤ ↑t.size → b⁻¹ • t.contourFunction ∈ K → ‖b⁻¹ • t.paperContourFunction - b⁻¹ • t.contourFunction‖ ≤ ε

Deterministic form with the modulus of continuity of an arbitrary compact set K of limit-candidate contours: on K, scaled contours with 1/ζ ≤ δ are ε-close in the two conventions.

theorem BGW.PlaneTree.exists_size_bound_norm_paper_sub_le' (K : Set C(↑unitInterval, ℝ)) (hK : IsCompact K) {ε : ℝ} (hε : 0 < ε) : ∃ (R : ℝ), ∀ (t : PlaneTree) (b : ℝ), R ≤ ↑t.size → b⁻¹ • t.paperContourFunction ∈ K → ‖b⁻¹ • t.paperContourFunction - b⁻¹ • t.contourFunction‖ ≤ ε

Symmetric form: the same bound when the paper contour lies in the compact set; used by the transfer from the paper convention to the library convention.

theorem BGW.ContinuumTrees.FiniteTree.tendsto_map_paperContour_of_tendsto_map_contour {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] (μ : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) (t : (n : ℕ) → Ω n → PlaneTree) (b : ℕ → ℝ) (hb : ∀ (n : ℕ), 0 < b n) (hF : ∀ (n : ℕ), Measurable fun (ω : Ω n) => (b n)⁻¹ • (t n ω).paperContourFunction) (hG : ∀ (n : ℕ), Measurable fun (ω : Ω n) => (b n)⁻¹ • (t n ω).contourFunction) (hsize : ∀ (R : ℝ), Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | ↑(t n ω).size < R}) Filter.atTop (nhds 0)) {ν : MeasureTheory.ProbabilityMeasure C(↑unitInterval, ℝ)} (hlim : Filter.Tendsto (fun (n : ℕ) => (μ n).map fun (ω : Ω n) => (b n)⁻¹ • (t n ω).contourFunction) Filter.atTop (nhds ν)) : Filter.Tendsto (fun (n : ℕ) => (μ n).map fun (ω : Ω n) => (b n)⁻¹ • (t n ω).paperContourFunction) Filter.atTop (nhds ν)

Law-level transfer, library convention → paper convention: if the tree sizes tend to infinity in probability and the divided library contours converge in law to ν, so do the divided paper contours. (The converse, with the roles exchanged, holds by the same proof.)

theorem BGW.ContinuumTrees.FiniteTree.tendsto_map_contour_of_tendsto_map_paperContour {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] (μ : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) (t : (n : ℕ) → Ω n → PlaneTree) (b : ℕ → ℝ) (hb : ∀ (n : ℕ), 0 < b n) (hF : ∀ (n : ℕ), Measurable fun (ω : Ω n) => (b n)⁻¹ • (t n ω).paperContourFunction) (hG : ∀ (n : ℕ), Measurable fun (ω : Ω n) => (b n)⁻¹ • (t n ω).contourFunction) (hsize : ∀ (R : ℝ), Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | ↑(t n ω).size < R}) Filter.atTop (nhds 0)) {ν : MeasureTheory.ProbabilityMeasure C(↑unitInterval, ℝ)} (hlim : Filter.Tendsto (fun (n : ℕ) => (μ n).map fun (ω : Ω n) => (b n)⁻¹ • (t n ω).paperContourFunction) Filter.atTop (nhds ν)) : Filter.Tendsto (fun (n : ℕ) => (μ n).map fun (ω : Ω n) => (b n)⁻¹ • (t n ω).contourFunction) Filter.atTop (nhds ν)

Law-level transfer, paper convention → library convention: the form consumed by tendsto_rooted_laws_of_contour when the contour input is stated as in the paper.

theorem BGW.ContinuumTrees.FiniteTree.tendsto_real_size_lt_of_ratio {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] (μ : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) (t : (n : ℕ) → Ω n → PlaneTree) (b : ℕ → ℝ) (hb : ∀ (n : ℕ), 0 < b n) (hbinfty : Filter.Tendsto b Filter.atTop Filter.atTop) (hratio : ∀ r > 0, Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | r < b n / ↑(t n ω).size}) Filter.atTop (nhds 0)) (R : ℝ) : Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | ↑(t n ω).size < R}) Filter.atTop (nhds 0)

The size-divergence hypothesis follows from the divisor-to-size tails of tendsto_rooted_laws_of_contour once the divisor tends to infinity.

measurability hypotheses hF, hG

PlaneTree is countable and carries no global MeasurableSpace; random trees are measurable for the explicit ⊤ σ-algebra, equivalently when every fibre t ⁻¹' {τ} is measurable.

theorem BGW.ContinuumTrees.FiniteTree.measurable_top_of_measurableSet_fibre {X : Type u_2} [MeasurableSpace X] (t : X → PlaneTree) (ht : ∀ (τ : PlaneTree), MeasurableSet (t ⁻¹' {τ})) : Measurable t

Measurability for ⊤ on PlaneTree is measurability of the fibres of singletons.

theorem BGW.ContinuumTrees.FiniteTree.measurable_comp_of_top {X : Type u_2} {Y : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] (t : X → PlaneTree) (ht : Measurable t) (f : PlaneTree → Y) : Measurable fun (x : X) => f (t x)

Any function of a ⊤-measurable random tree is measurable (so hF, hG hold for every tree observable).

theorem BGW.ContinuumTrees.FiniteTree.measurable_contour_of_top {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] {n : ℕ} (t : Ω n → PlaneTree) (b : ℝ) (ht : Measurable t) : Measurable fun (ω : Ω n) => b⁻¹ • (t ω).contourFunction

Hypothesis hG of tendsto_rooted_laws_of_contour.

theorem BGW.ContinuumTrees.FiniteTree.measurable_paperContour_of_top {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] {n : ℕ} (t : Ω n → PlaneTree) (b : ℝ) (ht : Measurable t) : Measurable fun (ω : Ω n) => b⁻¹ • (t ω).paperContourFunction

Hypothesis hG in the paper's time convention.

theorem BGW.ContinuumTrees.FiniteTree.measurable_rootedMeasuredGHSpace_of_top {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] {n : ℕ} (t : Ω n → PlaneTree) {b : ℝ} (hb : 0 < b) (ht : Measurable t) : Measurable fun (ω : Ω n) => MetricMeasure.RootedMeasuredGHSpace.scale b⁻¹ ⋯ (MetricMeasure.toRootedMeasuredGHSpace (rootedCompactMeasuredSpace (t ω)))

Hypothesis hF of tendsto_rooted_laws_of_contour.

the deterministic divisor of Remark 5.10

N n is the (deterministic) number of leaves, B n the stable normalizer, μ₀ > 0 the offspring mean parameter of the paper, θ > 0 the stability index; b n = N n / (μ₀^(1-1/θ) B n).

noncomputable def BGW.ContinuumTrees.FiniteTree.remarkDivisor (μ₀ θ : ℝ) (N : ℕ → ℕ) (B : ℕ → ℝ) (n : ℕ) : ℝ

The divisor of Remark 5.10.

Equations

• BGW.ContinuumTrees.FiniteTree.remarkDivisor μ₀ θ N B n = ↑(N n) / (μ₀ ^ (1 - 1 / θ) * B n)

theorem BGW.ContinuumTrees.FiniteTree.remarkDivisor_pos {μ₀ θ : ℝ} (hμ₀ : 0 < μ₀) {N : ℕ → ℕ} {B : ℕ → ℝ} (hN : ∀ (n : ℕ), 0 < N n) (hB : ∀ (n : ℕ), 0 < B n) (n : ℕ) : 0 < remarkDivisor μ₀ θ N B n

The divisor is positive.

theorem BGW.ContinuumTrees.FiniteTree.tendsto_remarkDivisor_atTop {μ₀ θ : ℝ} (hμ₀ : 0 < μ₀) {N : ℕ → ℕ} {B : ℕ → ℝ} (hN : ∀ (n : ℕ), 0 < N n) (hB : ∀ (n : ℕ), 0 < B n) (hNB : Filter.Tendsto (fun (n : ℕ) => B n / ↑(N n)) Filter.atTop (nhds 0)) : Filter.Tendsto (remarkDivisor μ₀ θ N B) Filter.atTop Filter.atTop

The divisor tends to infinity when B n = o(N n).

theorem BGW.ContinuumTrees.FiniteTree.tendsto_ratio_remarkDivisor {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] {μ₀ θ : ℝ} (hμ₀ : 0 < μ₀) {N : ℕ → ℕ} {B : ℕ → ℝ} (hN : ∀ (n : ℕ), 0 < N n) (hB : ∀ (n : ℕ), 0 < B n) (hBinfty : Filter.Tendsto B Filter.atTop Filter.atTop) (μ : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) (t : (n : ℕ) → Ω n → PlaneTree) (hsize : ∀ (c : ℝ), 0 < c → c < 1 / μ₀ → Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | ↑(t n ω).size < c * ↑(N n)}) Filter.atTop (nhds 0)) (r : ℝ) (hr : 0 < r) : Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | r < remarkDivisor μ₀ θ N B n / ↑(t n ω).size}) Filter.atTop (nhds 0)

The ratio hypothesis of tendsto_rooted_laws_of_contour for the divisor of Remark 5.10: if B n → ∞ and the number of vertices is at least c N n with probability tending to one for each c < 1/μ₀ (law of large numbers for the vertex/leaf ratio), then P(r < b_n/ζ_n) → 0 for every r > 0, because b_n/ζ ≈ μ₀^{1/θ}/B_n.