MetricLimit.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FKCRT.Inventory.crtScale line 13
Source documentation
The positive source normalization in original edge units.
```
def crtScale (P : Parameters) : ℝ := (actualOffspring P).sigma/(2*Real.sqrt 2*metricMean P)
```
Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.actualOffspring, OAI.FKCRT.Inventory.metricMean
lemma OAI.FKCRT.Inventory.crtScale_pos line 14
def OAI.FKCRT.Inventory.edgeScale line 17
lemma OAI.FKCRT.Inventory.edgeScale_pos line 18
def OAI.FKCRT.Inventory.heightFactor line 21
lemma OAI.FKCRT.Inventory.heightFactor_pos line 22
lemma OAI.FKCRT.Inventory.heightFactor_tendsto line 23
lemma OAI.FKCRT.Inventory.sqrt_size_ratio line 30
lemma OAI.FKCRT.Inventory.edgeScale_heightFactor line 47
lemma OAI.FKCRT.Inventory.edgeScale_sqrt_size_tendsto line 57
lemma OAI.FKCRT.TreeCoding.distribution_smul_one line 80
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.markedCodeLaw_map_fst line 109
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.marked_height_CLT line 120
abbrev OAI.FKCRT.Inventory.ActualDraw line 142
abbrev OAI.FKCRT.Inventory.actualDrawLaw line 143
def OAI.FKCRT.Inventory.actualHeight line 145

theorem OAI.FKCRT.Inventory.actualHeight_CLT line 150

Source documentation

The exact original-edge normalization of the same sampled marked tree has the standard (not rescaled) three-bridge excursion limit.

theorem actualHeight_CLT (P : Parameters)
    {Ω : Type} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    {B : Fin 3 → ℝ≥0 → Ω → ℝ} (hB : ∀ i,IsBrownianReal (B i) μ)
    (hI : iIndepFun (fun i ω t => B i t ω) μ) :
    TendstoInDistribution (actualHeight P) atTop (excursionPath B) (actualDrawLaw P) μ := by
…

Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.actualHeight, OAI.FKCRT.Inventory.actualDrawLaw

theorem OAI.FKCRT.TreeCoding.local_probability_transfer line 177

Source documentation

A compact-cover transfer lemma for varying discrete approximations. The local hypothesis is deterministic; only the stated error events vanish in probability. No independent coupling or random-cut independence is used.

theorem local_probability_transfer {E Ω' : Type*} {Ω : ℕ → Type*}
    [MetricSpace E] [CompleteSpace E] [SecondCountableTopology E]
    [MeasurableSpace E] [BorelSpace E]
    [∀ n,MeasurableSpace (Ω n)] [MeasurableSpace Ω']
    {μ : ∀ n,Measure (Ω n)} {ν : Measure Ω'} [∀ n,IsProbabilityMeasure (μ n)] [IsProbabilityMeasure ν]
    {X : ∀ n,Ω n → E} {Z : Ω' → E} (h : TendstoInDistribution X atTop Z μ ν)
    (hm : ∀ n,Measurable (X n)) (Y : ∀ n,Ω n → ℝ) (G : E → ℝ)
    (Bad : ∀ n,ℝ → Set (Ω n))
    (hBad : ∀ a,0<a → Tendsto (fun n => (μ n).real (Bad n a)) atTop (𝓝 0))
    (hloc : ∀ ε,0<ε → ∀ f : E,∃ r : ℝ,0<r ∧ ∃ a : ℝ,0<a ∧ ∃ N : ℕ,
      ∀ n≥N,∀ x : Ω n,dist (X n x) f<r → x∉Bad n a → |Y n x-G (X n x)| ≤ ε) :
    ∀ ε,0<ε → Tendsto (fun n => (μ n).real {x | ε < |Y n x-G (X n x)|}) atTop (𝓝 0) := by
…

theorem OAI.FKCRT.Inventory.CoreTree.marked_nearby_ghp_bound line 250

Source documentation

The same measured relation compares to a nearby deterministic path; this avoids presuming a triangle inequality for the presentation distance.

theorem marked_nearby_ghp_bound (P : Parameters) (n : ℕ)
    (x : MarkedCode (2*(n+1)+1)) (f : C(unitInterval,ℝ)) (a r η δ : ℝ) (hδ : 0<δ)
    (herr : ∀ j : Fin (2*(n+1)+1),
      |markedSpineSum coreIncrement x.val.1 j.isLt.le x.val.2-metricMean P*height x.val.1.val j.val| ≤
        a*Real.sqrt ((2*(n+1)+1:ℕ):ℝ))
    (hprox : dist (actualHeight P n x.val) f ≤ r)
    (hmod : ∀ s u,dist s u ≤ 1/(2*((n:ℝ)+1)) → |f s-f u| ≤ η)
    (hsmall : 4*edgeScale P n*((ofMarkedCode x).maxDegree:ℝ)+
      4*(edgeScale P n*a*Real.sqrt ((2*(n+1)+1:ℕ):ℝ)+r)+4*η ≤ 2*δ) :
    FKCRT.ghpEDist (FKCRT.treeSpace f)
      (FKCRT.mapSpace (edgeScale P n) ((FKCRT.rootedWordEquiv n).symm
        ((successfulMarkedEquiv n).symm x)).1) ≤ ENNReal.ofReal δ := by
…

Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.CoreTree.MarkedCode, OAI.FKCRT.Inventory.coreIncrement, OAI.FKCRT.Inventory.metricMean, OAI.FKCRT.Inventory.actualHeight, OAI.FKCRT.Inventory.edgeScale, OAI.FKCRT.Inventory.CoreTree.ofMarkedCode, OAI.FKCRT.Inventory.CoreTree.maxDegree, OAI.FKCRT.ghpEDist, OAI.FKCRT.treeSpace, OAI.FKCRT.mapSpace, OAI.FKCRT.rootedWordEquiv, OAI.FKCRT.Inventory.CoreTree.successfulMarkedEquiv

def OAI.FKCRT.Inventory.metricBad line 296
Source documentation
All and only the three exceptional events needed for the original map comparison: impossible marks (a null set), a macroscopic core, and a large uniform ancestral distance error.
```
def metricBad (P : Parameters) (n : ℕ) (a : ℝ) : Set (ActualDraw n) :=
…
```
Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.ActualDraw
lemma OAI.FKCRT.Inventory.metricBad_limit line 303
theorem OAI.FKCRT.Inventory.metric_test_local line 325
Source documentation
Local deterministic stability at every continuous limit path. This is the missing compact-cover interface, with the original map, exact degree mass, positive source normalization, and true bad events.
```
theorem metric_test_local (P : Parameters) (F : FKCRT.MetricMeasureData → ℝ)
    (hF : FKCRT.IsGHPTest F) (ε : ℝ) (hε : 0<ε) (f : C(unitInterval,ℝ)) :
    ∃ r : ℝ,0<r ∧ ∃ a : ℝ,0<a ∧ ∃ N : ℕ,∀ n≥N,∀ x : ActualDraw n,
      dist (actualHeight P n x) f<r → x∉metricBad P n a →
      |FKCRT.markedMapTest (edgeScale P n) n F x-F (FKCRT.treeSpace (actualHeight P n x))| ≤ ε := by
…
```
Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.MetricMeasureData, OAI.FKCRT.IsGHPTest, OAI.FKCRT.Inventory.ActualDraw, OAI.FKCRT.Inventory.actualHeight, OAI.FKCRT.Inventory.metricBad, OAI.FKCRT.markedMapTest, OAI.FKCRT.Inventory.edgeScale, OAI.FKCRT.treeSpace