Paper contour transfer for rooted measured convergence

Composition of the contour law convergence with the paper time convention and the divisor of Remark 5.10: convergence of the rescaled paper contour of random plane trees gives convergence of the laws of the rooted measured trees.

Reference: J.-F. Le Gall, Random trees and applications, Probab. Surveys 2 (2005).

theorem BGW.ContinuumTrees.FiniteTree.tendsto_rooted_laws_of_paperContour_remarkDivisor {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] (μ : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) (t : (n : ℕ) → Ω n → PlaneTree) (ht : ∀ (n : ℕ), Measurable (t n)) {μ₀ θ : ℝ} (hμ₀ : 0 < μ₀) {N : ℕ → ℕ} {B : ℕ → ℝ} (hN : ∀ (n : ℕ), 0 < N n) (hB : ∀ (n : ℕ), 0 < B n) (hBinfty : Filter.Tendsto B Filter.atTop Filter.atTop) (hNB : Filter.Tendsto (fun (n : ℕ) => B n / ↑(N n)) Filter.atTop (nhds 0)) (hsize : ∀ (c : ℝ), 0 < c → c < 1 / μ₀ → Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | ↑(t n ω).size < c * ↑(N n)}) Filter.atTop (nhds 0)) {ν : MeasureTheory.ProbabilityMeasure C(↑unitInterval, ℝ)} (hlim : Filter.Tendsto (fun (n : ℕ) => (μ n).map fun (ω : Ω n) => (remarkDivisor μ₀ θ N B n)⁻¹ • (t n ω).paperContourFunction) Filter.atTop (nhds ν)) : Filter.Tendsto (fun (n : ℕ) => (μ n).map fun (ω : Ω n) => MetricMeasure.RootedMeasuredGHSpace.scale (remarkDivisor μ₀ θ N B n)⁻¹ ⋯ (MetricMeasure.toRootedMeasuredGHSpace (rootedCompactMeasuredSpace (t n ω)))) Filter.atTop (nhds (ν.map Coding.rootedMeasuredGHSpace))

Rooted measured law convergence from the paper contour time convention, with the deterministic divisor of Remark 5.10.