Convergence.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FKCRT.Inventory.actual_map_tests line 15

Source documentation

The original map observable converges under its exact marked code law.

theorem actual_map_tests (P : Parameters)
    {Ω : Type} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    {B : Fin 3 → ℝ≥0 → Ω → ℝ} (hB : ∀ i,IsBrownianReal (B i) μ)
    (hI : iIndepFun (fun i ω t => B i t ω) μ)
    (F : FKCRT.MetricMeasureData → ℝ) (hF : FKCRT.IsGHPTest F) :
    Tendsto (fun n => ∫ x,FKCRT.markedMapTest (edgeScale P n) n F x ∂actualDrawLaw P n)
      atTop (𝓝 (FKCRT.brownianExpectation μ B F)) := by
…

Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.MetricMeasureData, OAI.FKCRT.IsGHPTest, OAI.FKCRT.markedMapTest, OAI.FKCRT.Inventory.edgeScale, OAI.FKCRT.Inventory.actualDrawLaw, OAI.FKCRT.brownianExpectation

theorem OAI.FKCRT.finite_fk_maps_converge_to_brownian_crt line 68
Source documentation
GHP convergence of the finite FK laws to the standard Brownian-excursion CRT, through every positive edge count.
Distinct definitions of this name: ComparatorChallenges/FKCRT.lean:208 (same statement text; different proof or body). Qualify references as OAI.FKCRT.finite_fk_maps_converge_to_brownian_crt@path.
```
theorem finite_fk_maps_converge_to_brownian_crt : MainStatement := by
…
```
Mentions: OAI.FKCRT.MainStatement