GHPBounds.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FKCRT.TreeCoding.heightProjection line 19
Source documentation
Second continuous coordinate of the actual joint coding.
```
def heightProjection (f : C(unitInterval,ℝ×ℝ)) : C(unitInterval,ℝ) :=
…
```
lemma OAI.FKCRT.TreeCoding.heightProjection_continuous line 22
lemma OAI.FKCRT.TreeCoding.heightProjection_diagonal line 25
def OAI.FKCRT.TreeCoding.heightCode line 30
Source documentation
Actual normalized preorder height path, including both endpoint cells.
```
def heightCode {N : ℕ} (p : CriticalEvenOffspring) (d : Code N) : C(unitInterval,ℝ) :=
…
```
Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.Code
lemma OAI.FKCRT.TreeCoding.heightCode_eq line 33

theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.heightCode_CLT line 38

Source documentation

The unconditional, full height-path limit with the exact excursion law; this only reuses the already proved joint invariance theorem.

theorem CriticalEvenOffspring.heightCode_CLT (p : CriticalEvenOffspring)
    {Ω : Type} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : Fin 3 → ℝ≥0 → Ω → ℝ} (hB : ∀ i,IsBrownianReal (B i) P)
    (hI : iIndepFun (fun i ω t => B i t ω) P) :
    TendstoInDistribution (fun n (d : Code (2*n+1)) => heightCode p d) atTop
      (excursionPath B) p.codeLaw P := by
…

Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.Code, OAI.FKCRT.TreeCoding.heightCode, OAI.FKCRT.TreeCoding.excursionPath

theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.heightCRT_tests line 53

Source documentation

Continuous-tree observables converge under the genuine code law.

theorem CriticalEvenOffspring.heightCRT_tests (p : CriticalEvenOffspring)
    {Ω : Type} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : Fin 3 → ℝ≥0 → Ω → ℝ} (hB : ∀ i,IsBrownianReal (B i) P)
    (hI : iIndepFun (fun i ω t => B i t ω) P)
    (F : FKCRT.MetricMeasureData → ℝ) (hF : FKCRT.IsGHPTest F) :
    Tendsto (fun n => ∫ d,F (FKCRT.treeSpace (heightCode p d)) ∂p.codeLaw n) atTop
      (𝓝 (FKCRT.brownianExpectation P B F)) := by
…

Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.MetricMeasureData, OAI.FKCRT.IsGHPTest, OAI.FKCRT.treeSpace, OAI.FKCRT.TreeCoding.heightCode, OAI.FKCRT.brownianExpectation

lemma OAI.FKCRT.Inventory.CoreTree.maxDegree_le_iff line 80
lemma OAI.FKCRT.Inventory.CoreTree.maxDegree_le_ofMarkedCode line 97
lemma OAI.FKCRT.Inventory.CoreTree.maxDegree_large_ofMarkedCode line 105
lemma OAI.FKCRT.Inventory.CoreTree.nodePoint_gridPoint line 132
lemma OAI.FKCRT.Inventory.CoreTree.heightCode_nodePoint line 137

lemma OAI.FKCRT.Inventory.CoreTree.route_heightCode_fit line 142

Source documentation

Normalized marked error is evaluated at exactly the same coding mesh.

lemma route_heightCode_fit (p : CriticalEvenOffspring) (t : CoreTree) (β scale a : ℝ)
    (hs : 0 ≤ scale)
    (herr : ∀ v,|(t.routeLength v:ℝ)-β*t.depth v| ≤ a*Real.sqrt t.labels.length) :
    ∀ v,|scale*(t.routeLength v:ℝ)-
      ((scale*β*2*Real.sqrt t.labels.length/p.sigma) • heightCode p t.toCode) (t.nodePoint v)| ≤
        scale*a*Real.sqrt t.labels.length := by
…

Mentions: OAI.FKCRT.Inventory.CoreTree

theorem OAI.FKCRT.Inventory.CoreTree.heightCode_ghp_bound line 160

Source documentation

Direct genuine-map GHP bound in the actual normalized height path.

theorem heightCode_ghp_bound (p : CriticalEvenOffspring) (t : CoreTree)
    {n : ℕ} (w : FKCRT.SuccessfulWord n) (hw : t.word=List.ofFn w.val)
    (β scale a η δ : ℝ) (hs : 0<scale) (hδ : 0<δ)
    (herr : ∀ v,|(t.routeLength v:ℝ)-β*t.depth v| ≤ a*Real.sqrt t.labels.length)
    (hmod : ∀ s u,dist s u ≤ 1/(t.word.length:ℝ) →
      |((scale*β*2*Real.sqrt t.labels.length/p.sigma) • heightCode p t.toCode) s-
        ((scale*β*2*Real.sqrt t.labels.length/p.sigma) • heightCode p t.toCode) u| ≤ η)
    (hsmall : 4*scale*(t.maxDegree:ℝ)+4*(scale*a*Real.sqrt t.labels.length)+4*η ≤ 2*δ) :
    FKCRT.ghpEDist
      (FKCRT.treeSpace ((scale*β*2*Real.sqrt t.labels.length/p.sigma) • heightCode p t.toCode))
      (FKCRT.mapSpace scale ((FKCRT.rootedWordEquiv n).symm w).1) ≤ ENNReal.ofReal δ := by
…

Mentions: OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.SuccessfulWord, OAI.FKCRT.ghpEDist, OAI.FKCRT.treeSpace, OAI.FKCRT.mapSpace, OAI.FKCRT.rootedWordEquiv

lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.code_event_probability line 185
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.actual_max_degree line 195
theorem OAI.FKCRT.Inventory.actual_max_core line 211
Source documentation
The actual largest core has vanishing square-root scale, under the original compatible marked law. Impossible marks are not sampled.
```
theorem actual_max_core (P : Parameters) {ε : ℝ} (hε : 0<ε) :
    Tendsto (fun n => ((actualOffspring P).markedCodeLaw
      (fun k => (CoreLabel.markLaw P k).toMeasure) n).real
      {x | ∃ h : ∀ i,(x.2 i).arity=(x.1.val i).val,
        ε*Real.sqrt ((2*n+1:ℕ):ℝ)<((CoreTree.ofMarkedCode ⟨x,h⟩).maxDegree:ℝ)}) atTop (𝓝 0) := by
…
```
Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.actualOffspring, OAI.FKCRT.Inventory.CoreLabel.markLaw, OAI.FKCRT.Inventory.CoreTree.ofMarkedCode
lemma OAI.FKCRT.Inventory.CoreTree.code_marks_of_labels line 234
lemma OAI.FKCRT.Inventory.CoreTree.marked_route_error line 249
lemma OAI.FKCRT.Inventory.CoreTree.marked_heightCode line 265
lemma OAI.FKCRT.Inventory.CoreTree.ofMarkedCode_word_successful line 275

theorem OAI.FKCRT.Inventory.CoreTree.marked_height_ghp_bound line 283

Source documentation

The full deterministic measured comparison for a genuine marked draw: no independent copy of the tree, changed metric, or approximate degree law.

theorem marked_height_ghp_bound (p : CriticalEvenOffspring) (n : ℕ)
    (x : MarkedCode (2*(n+1)+1)) (β scale a η δ : ℝ) (hs : 0<scale) (hδ : 0<δ)
    (herr : ∀ j : Fin (2*(n+1)+1),
      |markedSpineSum coreIncrement x.val.1 j.isLt.le x.val.2-β*height x.val.1.val j.val| ≤
        a*Real.sqrt ((2*(n+1)+1:ℕ):ℝ))
    (hmod : ∀ s u,dist s u ≤ 1/(2*((n:ℝ)+1)) →
      |((scale*β*2*Real.sqrt ((2*(n+1)+1:ℕ):ℝ)/p.sigma) • heightCode p x.val.1) s-
        ((scale*β*2*Real.sqrt ((2*(n+1)+1:ℕ):ℝ)/p.sigma) • heightCode p x.val.1) u| ≤ η)
    (hsmall : 4*scale*((ofMarkedCode x).maxDegree:ℝ)+
      4*(scale*a*Real.sqrt ((2*(n+1)+1:ℕ):ℝ))+4*η ≤ 2*δ) :
    FKCRT.ghpEDist
      (FKCRT.treeSpace ((scale*β*2*Real.sqrt ((2*(n+1)+1:ℕ):ℝ)/p.sigma) • heightCode p x.val.1))
…

Mentions: OAI.FKCRT.Inventory.CoreTree.MarkedCode, OAI.FKCRT.Inventory.coreIncrement, OAI.FKCRT.Inventory.CoreTree.ofMarkedCode, OAI.FKCRT.Inventory.CoreTree.maxDegree, OAI.FKCRT.ghpEDist, OAI.FKCRT.treeSpace