Exact-size height and contour laws

The paper clock uses twice the number of vertices. The library clock uses twice the number of edges. In both laws the height and contour come from the same tree.

noncomputable def BGW.StableTrees.ExactContour.treeContourLin (τ : LocallyFinite.Tree) (s : ℝ) : ℝ

The interpolated contour (original speed, 0 after time 2(z-1)) of the decoded finite tree; 0 for an infinite tree.

Equations

• BGW.StableTrees.ExactContour.treeContourLin τ s = if h : BGW.LocallyFinite.FiniteVertices τ then (BGW.PlaneTree.equivFiniteVertices.symm ⟨τ, h⟩).contourLin s else 0

theorem BGW.StableTrees.ExactContour.continuous_treeContourLin (τ : LocallyFinite.Tree) : Continuous (treeContourLin τ)

The interpolated tree contour is continuous (the junk branch of treeContourPath never occurs).

noncomputable def BGW.StableTrees.ExactContour.treeContourPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (τ : LocallyFinite.Tree) : C(↑(Set.Icc 0 ↑T), ℝ)

Tree contour path on [0,T]: t ↦ (B n / n) * treeContourLin τ (2 n t); junk 0 if the interpolation were discontinuous (never, continuous_treeContourLin).

Equations

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

noncomputable def BGW.StableTrees.ExactContour.heightContourPath (B : ℕ → ℝ) (n : ℕ) (τ : LocallyFinite.Tree) : C(↑(Set.Icc 0 1), ℝ) × C(↑(Set.Icc 0 1), ℝ)

The (height, contour) pair path on [0,1] at time scales nt and 2nt, amplitude B n / n for both.

Equations

• BGW.StableTrees.ExactContour.heightContourPath B n τ = (BGW.StableTrees.TailPair.treeHeightPath B n 1 τ, BGW.StableTrees.ExactContour.treeContourPath B n 1 τ)

noncomputable def BGW.StableTrees.ExactContour.exactHeightContourLaw (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (_hn : Admissible μ n) : MeasureTheory.ProbabilityMeasure (C(↑(Set.Icc 0 1), ℝ) × C(↑(Set.Icc 0 1), ℝ))

The exact-size height/contour law on [0,1]: height and contour of ONE BGW tree conditioned on size exactly n (sealed K02 exactTreeLaw, totalized).

Equations

• BGW.StableTrees.ExactContour.exactHeightContourLaw μ B n _hn = (BGW.StableTrees.DiscreteForest.exactTreeLaw μ n).map (BGW.StableTrees.ExactContour.heightContourPath B n)

noncomputable def BGW.StableTrees.ExactContour.contourHeightError (B : ℕ → ℝ) (n : ℕ) (a : NNReal) (τ : LocallyFinite.Tree) : ℝ

The uniform distance on [0,a] between the normalized contour at time 2nt and the normalized interpolated height at time nt, for one tree.

Equations

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

noncomputable def BGW.StableTrees.ExactContour.heightLibContourPath (B : ℕ → ℝ) (n : ℕ) (τ : LocallyFinite.Tree) : C(↑(Set.Icc 0 1), ℝ) × C(↑(Set.Icc 0 1), ℝ)

The (height, contour) pair in the library contour convention (s ↦ C(2(z-1)s), sealed PlaneTree.contourFunction), scaled by B n / n; 0 contour for an infinite tree.

Equations

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

theorem BGW.StableTrees.ExactContour.measurable_heightLibContourPath (B : ℕ → ℝ) (n : ℕ) : Measurable (heightLibContourPath B n)

Measurability guard for the library-clock pair (Sol audit k13k16, finding 4).

noncomputable def BGW.StableTrees.ExactContour.exactHeightLibContourLaw (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (_hn : Admissible μ n) : MeasureTheory.ProbabilityMeasure (C(↑(Set.Icc 0 1), ℝ) × C(↑(Set.Icc 0 1), ℝ))

The exact-size height/contour law in the library contour convention.

Equations

• BGW.StableTrees.ExactContour.exactHeightLibContourLaw μ B n _hn = (BGW.StableTrees.DiscreteForest.exactTreeLaw μ n).map (BGW.StableTrees.ExactContour.heightLibContourPath B n)

theorem BGW.StableTrees.ExactContour.measurable_treeContourPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : Measurable (treeContourPath B n T)

The contour path is a measurable observable of the tree.

theorem BGW.StableTrees.ExactContour.measurable_heightContourPath (B : ℕ → ℝ) (n : ℕ) : Measurable (heightContourPath B n)

The height and contour of one tree form a measurable pair.

theorem BGW.StableTrees.ExactContour.treeContourLin_treeMirror (t : PlaneTree) {s : ℝ} (hs0 : 0 ≤ s) (hs : s ≤ 2 * (↑t.size - 1)) : treeContourLin (treeMirror t.toLocallyFinite) s = treeContourLin t.toLocallyFinite (2 * (↑t.size - 1) - s)

The mirrored tree's contour is the reflected contour (the LocallyFinite form of PlaneTree.contourLin_mirror).

theorem BGW.StableTrees.ExactContour.treeContourLin_toLocallyFinite (t : PlaneTree) (s : ℝ) : treeContourLin t.toLocallyFinite s = t.contourLin s

On a finite tree, decoding the contour returns the original polygonal contour.

theorem BGW.StableTrees.ExactContour.treeContourPath_toLocallyFinite (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (t : PlaneTree) (s : ↑(Set.Icc 0 ↑T)) : (treeContourPath B n T t.toLocallyFinite) s = B n / ↑n * t.contourLin (2 * ↑n * ↑s)

On a finite tree the contour path evaluates at the paper clock.

theorem BGW.StableTrees.ExactContour.treeContourPath_eq_paperContourFunction (B : ℕ → ℝ) {n : ℕ} (t : PlaneTree) (ht : t.size = n) (s : ↑unitInterval) : (treeContourPath B n 1 t.toLocallyFinite) s = B n / ↑n * t.paperContourFunction s

Paper convention, exactly: for a tree of size n the contour path at scale 2nt is (B n / n) times the sealed PlaneTree.paperContourFunction (s ↦ C_{2ζ s}).

theorem BGW.StableTrees.ExactContour.abs_treeContourPath_sub_contourFunction_le (B : ℕ → ℝ) {n : ℕ} (t : PlaneTree) (ht : t.size = n) (s : ↑unitInterval) : |(treeContourPath B n 1 t.toLocallyFinite) s - B n / ↑n * t.contourFunction s| ≤ 2 * |B n / ↑n|

Library convention (2(n-1)t, sealed PlaneTree.contourFunction): uniformly within 2 |B n / n| of the 2nt convention.