OAI/Probability/FKMaps/HeightTightness.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FKCRT.TreeCoding.codeEmbedding line 10
2. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.code_probability_le_stream line 14
3. lemma OAI.FKCRT.TreeCoding.recordHeight_congr_prefix line 65
4. def OAI.FKCRT.TreeCoding.codeHeightModulusFailure line 77
5. lemma OAI.FKCRT.TreeCoding.codeHeightModulusFailure_stream line 82
6. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.code_height_modulus_bound line 97
7. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.code_geometric_vanish line 115
8. abbrev OAI.FKCRT.TreeCoding.ClosePairs line 155
9. instance OAI.FKCRT.TreeCoding.(instance at line 157) line 157
10. def OAI.FKCRT.TreeCoding.oscillationPath line 160
11. def OAI.FKCRT.TreeCoding.pathOscillation line 163
12. lemma OAI.FKCRT.TreeCoding.pathOscillation_nonneg line 165
13. lemma OAI.FKCRT.TreeCoding.pathOscillation_le line 167
14. lemma OAI.FKCRT.TreeCoding.sub_le_pathOscillation line 173
15. lemma OAI.FKCRT.TreeCoding.pathOscillation_lipschitz line 177
16. lemma OAI.FKCRT.TreeCoding.pathOscillation_vanish line 197
17. def OAI.FKCRT.TreeCoding.oscillationGauge line 215
18. lemma OAI.FKCRT.TreeCoding.oscillationGauge_continuous line 217
19. lemma OAI.FKCRT.TreeCoding.oscillationGauge_nonneg line 220
20. lemma OAI.FKCRT.TreeCoding.oscillationGauge_abs_le line 223
21. lemma OAI.FKCRT.TreeCoding.oscillationGauge_integral_vanish line 228
22. lemma OAI.FKCRT.TreeCoding.oscillation_probability_le_gauge line 243
23. lemma OAI.FKCRT.TreeCoding.continuousPath_modulus_tight line 261
24. lemma OAI.FKCRT.TreeCoding.height_pair_control line 286
25. lemma OAI.FKCRT.TreeCoding.error_le_error_add line 306
26. lemma OAI.FKCRT.TreeCoding.badHeightFraction_interval_lower line 316
27. lemma OAI.FKCRT.TreeCoding.uniform_error_of_average line 340
28. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.codeWalk_converges line 378
29. lemma OAI.FKCRT.TreeCoding.gridPoint_dist_le line 395
30. lemma OAI.FKCRT.TreeCoding.walk_grid_oscillation line 407
31. lemma OAI.FKCRT.TreeCoding.floor_fraction_bounds line 418
32. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bad_fraction_markov line 442
33. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.uniform_height_error_limit line 454

    Source documentation

    Exact conditioned critical finite-variance height/walk coupling, uniformly at every depth-first vertex. Only the stated second moment is used.

    theorem CriticalEvenOffspring.uniform_height_error_limit (p : CriticalEvenOffspring)
        {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
        {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P) {ε : ℝ} (hε : 0<ε) :
        Tendsto (fun n => (p.codeLaw n).real {d | ∃ j<2*n+1,
          ε*Real.sqrt ((2*n+1:ℕ):ℝ)< |(walk d.val j:ℝ)-(p.variance/2)*height d.val j|})
          atTop (𝓝 0) := by
    …

    Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.walk, OAI.FKCRT.TreeCoding.height

34. theorem OAI.FKCRT.TreeCoding.tendstoInDistribution_of_close line 556

    Source documentation

    Converging together with varying sample spaces and actual probability laws.

    theorem tendstoInDistribution_of_close {E Ω' : Type*} {Ω : ℕ → Type*}
        [PseudoMetricSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
        [∀ n, MeasurableSpace (Ω n)] [MeasurableSpace Ω']
        {μ : ∀ n, Measure (Ω n)} {ν : Measure Ω'} [∀ n, IsProbabilityMeasure (μ n)]
        [IsProbabilityMeasure ν] {X Y : ∀ n, Ω n → E} {Z : Ω' → E}
        (hXZ : TendstoInDistribution X atTop Z μ ν)
        (hY : ∀ n, AEMeasurable (Y n) (μ n))
        (hclose : ∀ ε>0, Tendsto (fun n => (μ n).real {ω | ε < dist (X n ω) (Y n ω)}) atTop (𝓝 0)) :
        TendstoInDistribution Y atTop Z μ ν := by
    …

35. def OAI.FKCRT.TreeCoding.diagonalPath line 604
36. lemma OAI.FKCRT.TreeCoding.diagonalPath_lipschitz line 606
37. lemma OAI.FKCRT.TreeCoding.jointCode_close line 615
38. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.joint_diagonal_close line 641
39. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.jointCode_vervaat_CLT line 666

    Source documentation

    Full joint walk/height convergence to the same Vervaat bridge excursion. Identification with the standard Bessel3 excursion uses its finite-dimensional laws.

    theorem CriticalEvenOffspring.jointCode_vervaat_CLT (p : CriticalEvenOffspring)
        {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
        {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P) :
        TendstoInDistribution (fun n (d : Code (2*n+1)) => jointCode p.sigma d) atTop
          (fun ω => diagonalPath (vervaat (bridgePath B ω))) p.codeLaw P := by
    …

    Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.Code, OAI.FKCRT.TreeCoding.jointCode, OAI.FKCRT.TreeCoding.diagonalPath, OAI.FKCRT.TreeCoding.vervaat, OAI.FKCRT.TreeCoding.bridgePath