OAI/Probability/FKMaps/ExcursionLaw.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FKCRT.SimpleWalk.sum_differences_real line 11
2. lemma OAI.FKCRT.SimpleWalk.remaining_differences line 23
3. lemma OAI.FKCRT.SimpleWalk.durationRatio_bridge line 42
4. lemma OAI.FKCRT.SimpleWalk.durationVariance_bridge line 50
5. lemma OAI.FKCRT.Histogram.lintegral_min_tendsto line 69

   Source documentation

   Scheffé's argument in its nonnegative measure-theoretic form: pointwise convergence of probability densities implies convergence of every bounded test.

   lemma lintegral_min_tendsto {α : Type*} [MeasurableSpace α] {μ : Measure α}
       {f : ℕ → α → ℝ≥0∞} {g : α → ℝ≥0∞}
       (hf : ∀ n, Measurable (f n)) (hg : Measurable g)
       (hlim : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x)))
       (hgint : ∫⁻ x,g x ∂μ≠∞) :
       Tendsto (fun n => ∫⁻ x,min (f n x) (g x) ∂μ) atTop (𝓝 (∫⁻ x,g x ∂μ)) := by
   …

6. lemma OAI.FKCRT.Histogram.tendsto_withDensity line 82
7. lemma OAI.FKCRT.SimpleWalk.pathMass_trace_at_size line 109
8. lemma OAI.FKCRT.SimpleWalk.excursion_probability line 115
9. def OAI.FKCRT.SimpleWalk.mesh line 128

   Source documentation

   Lattice mesh and actual sampled heights, not a reference density.

   def mesh (n : ℕ) : ℝ := 2/Real.sqrt ((2*n+1:ℕ):ℝ)

10. def OAI.FKCRT.SimpleWalk.gridIndex line 130
11. def OAI.FKCRT.SimpleWalk.gridSample line 134
12. def OAI.FKCRT.SimpleWalk.histogramDensity line 137
13. lemma OAI.FKCRT.SimpleWalk.mesh_pos line 140
14. lemma OAI.FKCRT.SimpleWalk.odd_size_atTop line 142
15. lemma OAI.FKCRT.SimpleWalk.mesh_tendsto_zero line 145
16. lemma OAI.FKCRT.SimpleWalk.index_eq_iff line 149
17. lemma OAI.FKCRT.SimpleWalk.gridSample_eq line 166
18. lemma OAI.FKCRT.SimpleWalk.gridIndex_probability line 174
19. lemma OAI.FKCRT.SimpleWalk.histogramDensity_positive line 185
20. lemma OAI.FKCRT.SimpleWalk.gridRemainder_atTop line 214
21. lemma OAI.FKCRT.SimpleWalk.histogramDensity_limit_pos line 223
22. lemma OAI.FKCRT.SimpleWalk.chainDensity_zero line 249
23. lemma OAI.FKCRT.SimpleWalk.histogramDensity_limit_ae line 261
24. lemma OAI.FKCRT.Radial.aemeasurable_standardExcursion line 291
25. lemma OAI.FKCRT.Radial.standardExcursion_hasLaw line 299
26. lemma OAI.FKCRT.Radial.bridgeDensity_probability line 315
27. lemma OAI.FKCRT.SimpleWalk.pathSum_step line 338
28. lemma OAI.FKCRT.SimpleWalk.abs_sign line 348
29. lemma OAI.FKCRT.SimpleWalk.pathSum_diff_le line 350
30. lemma OAI.FKCRT.SimpleWalk.pathSum_dist_le line 370
31. def OAI.FKCRT.SimpleWalk.simplePolygon line 377
32. def OAI.FKCRT.SimpleWalk.arrayPolygon line 380
33. lemma OAI.FKCRT.SimpleWalk.arrayPolygon_binaryArray line 383
34. lemma OAI.FKCRT.SimpleWalk.arrayPolygon_code line 387
35. lemma OAI.FKCRT.SimpleWalk.simplePolygon_grid_bound line 391
36. lemma OAI.FKCRT.SimpleWalk.code_simple_integral line 409
37. lemma OAI.FKCRT.SimpleWalk.histogram_probability line 427
38. lemma OAI.FKCRT.SimpleWalk.histogram_converges line 433
39. lemma OAI.FKCRT.SimpleWalk.grid_integral_limit line 442
40. def OAI.FKCRT.SimpleWalk.pathEvaluation line 458
41. lemma OAI.FKCRT.SimpleWalk.pathEvaluation_continuous line 461
42. lemma OAI.FKCRT.SimpleWalk.polygon_integral_close line 464
43. lemma OAI.FKCRT.SimpleWalk.polygon_integral_limit line 481
44. lemma OAI.FKCRT.SimpleWalk.vervaat_fdd line 495
45. def OAI.FKCRT.TreeCoding.interiorTimes line 533

    Source documentation

    Strictly interior mesh, with the initial zero included only as a reference.

    def interiorTimes (m : ℕ) (i : Fin (m+2)) : unitInterval :=
    …

46. lemma OAI.FKCRT.TreeCoding.interiorTimes_strictMono line 536
47. lemma OAI.FKCRT.TreeCoding.interiorTimes_zero line 541
48. lemma OAI.FKCRT.TreeCoding.interiorTimes_lt_one line 545
49. def OAI.FKCRT.TreeCoding.interiorIndex line 549
50. def OAI.FKCRT.TreeCoding.interiorReconstruct line 551
51. lemma OAI.FKCRT.TreeCoding.continuous_interiorReconstruct line 554
52. lemma OAI.FKCRT.TreeCoding.interiorIndex_bounds line 557
53. lemma OAI.FKCRT.TreeCoding.interiorTime_dist line 563
54. lemma OAI.FKCRT.TreeCoding.interiorReconstruct_tendsto line 575
55. lemma OAI.FKCRT.TreeCoding.interior_integral_limit line 600
56. lemma OAI.FKCRT.TreeCoding.identDistrib_of_interior line 617
57. lemma OAI.FKCRT.TreeCoding.continuous_standardExcursion line 643
58. lemma OAI.FKCRT.TreeCoding.standardExcursion_ae_continuous line 654
59. def OAI.FKCRT.TreeCoding.excursionPath line 660
60. lemma OAI.FKCRT.TreeCoding.excursionPath_ae_eq line 663
61. lemma OAI.FKCRT.TreeCoding.dense_eval_measurableEmbedding line 670
62. lemma OAI.FKCRT.TreeCoding.excursionPath_aemeasurable line 678
63. theorem OAI.FKCRT.TreeCoding.vervaat_identDistrib_excursion line 690

    Source documentation

    The law identification is proved from exact binary first-passage counts and radial Gaussian densities, not assumed as Vervaat's theorem.

    theorem vervaat_identDistrib_excursion {Ω : Type} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
        {W : ℝ≥0 → Ω → ℝ} (hW : IsBrownianReal W P)
        {B : Fin 3 → ℝ≥0 → Ω → ℝ} (hB : ∀ i,IsBrownianReal (B i) P)
        (hI : iIndepFun (fun i ω t => B i t ω) P) :
        IdentDistrib (fun ω => vervaat (bridgePath W ω)) (excursionPath B) P P := by
    …

    Mentions: OAI.FKCRT.TreeCoding.vervaat, OAI.FKCRT.TreeCoding.bridgePath, OAI.FKCRT.TreeCoding.excursionPath

64. lemma OAI.FKCRT.TreeCoding.diagonalExcursion_eq line 707
65. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.jointCodingStatement line 714

    Source documentation

    The exact full joint finite-variance tree-coding theorem with the frozen standard normalized (three-independent-bridge norm) excursion.

    theorem CriticalEvenOffspring.jointCodingStatement (p : CriticalEvenOffspring) : JointCodingStatement p := by
    …

    Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.JointCodingStatement