OAI/Probability/FKMaps/ExcursionGeometry.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FKCRT.interval_image_bddBelow line 11
2. lemma OAI.FKCRT.interval_inf_le_left line 15
3. lemma OAI.FKCRT.interval_inf_le_right line 19
4. lemma OAI.FKCRT.excursionDist_self line 23
5. lemma OAI.FKCRT.excursionDist_comm line 27
6. lemma OAI.FKCRT.excursionDist_nonneg line 32
7. lemma OAI.FKCRT.interval_inf_ge_min line 39
8. lemma OAI.FKCRT.excursionDist_triangle line 51
9. lemma OAI.FKCRT.excursionDist_eq_of_zero_left line 64
10. lemma OAI.FKCRT.excursionDist_zero_of_eqvGen line 73
11. lemma OAI.FKCRT.treeProjection_surjective line 88
12. lemma OAI.FKCRT.excursionDist_out line 91
13. def OAI.FKCRT.excursionTreeMetric line 103

    Source documentation

    The excursion quotient, with the genuine induced metric.

    def excursionTreeMetric {e : unitInterval → ℝ} (he : Continuous e) :
        MetricSpace (ExcursionTree e) where
    …

    Mentions: OAI.FKCRT.ExcursionTree

14. lemma OAI.FKCRT.unitInterval_dist_le_of_mem_uIcc line 113
15. lemma OAI.FKCRT.treeProjection_continuous line 130
16. lemma OAI.FKCRT.excursionTree_topology line 155
17. lemma OAI.FKCRT.excursionTree_compact line 163
18. lemma OAI.FKCRT.unitInterval_volume_univ line 172
19. lemma OAI.FKCRT.treeSpace_mass_univ line 179
20. lemma OAI.FKCRT.treeSpace_valid line 192

    Source documentation

    A continuous excursion codes a compact metric probability space. No positivity or endpoint hypotheses are required for this validity statement.

    lemma treeSpace_valid {e : unitInterval → ℝ} (he : Continuous e) : (treeSpace e).Valid := by
    …

    Mentions: OAI.FKCRT.treeSpace

21. lemma OAI.FKCRT.interval_inf_sub_le line 200
22. lemma OAI.FKCRT.interval_inf_abs_sub_le line 212
23. lemma OAI.FKCRT.excursionDist_abs_sub_le line 224

    Source documentation

    Deterministic four-times-sup-norm distortion bound for excursion coding.

    lemma excursionDist_abs_sub_le {e f : unitInterval → ℝ}
        (he : Continuous e) (hf : Continuous f) (s t : unitInterval) {ε : ℝ}
        (h : ∀ r, |e r - f r| ≤ ε) :
        |excursionDist e s t - excursionDist f s t| ≤ 4 * ε := by
    …

    Mentions: OAI.FKCRT.excursionDist

24. lemma OAI.FKCRT.levyProkhorovEDist_map_le_of_dist line 236
25. lemma OAI.FKCRT.ghpEDist_le_of_coding line 262

    Source documentation

    A common coding with distortion at most 2ε and a common mass gives GHP distance at most ε. The metric-quotient gluing is supplied by Mathlib.

    lemma ghpEDist_le_of_coding {X Y : MetricMeasureData}
        (hX : X.Valid) (hY : Y.Valid) {Z : Type} [Nonempty Z] [MeasurableSpace Z]
        (μ : Measure Z) (f : Z → X.Carrier) (g : Z → Y.Carrier)
        (hf : @Measurable _ _ inferInstance X.measurableSpace f)
        (hg : @Measurable _ _ inferInstance Y.measurableSpace g)
        (hsf : Function.Surjective f) (hsg : Function.Surjective g)
        (hmf : @Measure.map _ _ inferInstance X.measurableSpace f μ = X.mass)
        (hmg : @Measure.map _ _ inferInstance Y.measurableSpace g μ = Y.mass)
        {ε : ℝ} (hε : 0 < ε)
        (hfg : ∀ s t, |X.distance (f s) (f t) - Y.distance (g s) (g t)| ≤ 2 * ε) :
        ghpEDist X Y ≤ ENNReal.ofReal ε := by
    …

    Mentions: OAI.FKCRT.MetricMeasureData, OAI.FKCRT.ghpEDist

26. lemma OAI.FKCRT.graph_connected line 312
27. def OAI.FKCRT.mapMetric line 316
28. lemma OAI.FKCRT.degreeMass_univ line 331
29. lemma OAI.FKCRT.mapSpace_valid line 341
30. lemma OAI.FKCRT.fkWeight_pos line 352
31. lemma OAI.FKCRT.partition_nonneg line 355
32. lemma OAI.FKCRT.treeProjection_measurable line 359
33. lemma OAI.FKCRT.ghpEDist_treeSpace_le line 369

    Source documentation

    The excursion-to-measured-tree map preserves the exact uniform-time mass.

    lemma ghpEDist_treeSpace_le {e f : unitInterval → ℝ}
        (he : Continuous e) (hf : Continuous f) {ε : ℝ} (hε : 0 < ε)
        (h : ∀ t, |e t - f t| ≤ ε) :
        ghpEDist (treeSpace e) (treeSpace f) ≤ ENNReal.ofReal (2 * ε) := by
    …

    Mentions: OAI.FKCRT.ghpEDist, OAI.FKCRT.treeSpace

34. lemma OAI.FKCRT.IsGHPTest.continuous_treeSpace line 383
35. lemma OAI.FKCRT.continuous_standardExcursion line 401
36. lemma OAI.FKCRT.standardExcursion_nonneg line 414
37. lemma OAI.FKCRT.standardExcursion_one line 417
38. lemma OAI.FKCRT.standardExcursion_zero line 422
39. lemma OAI.FKCRT.standardExcursion_ae_continuous line 427
40. lemma OAI.FKCRT.standardExcursion_ae_zero line 434
41. lemma OAI.FKCRT.standardExcursion_treeSpace_ae_valid line 441
42. def OAI.FKCRT.standardExcursionPath line 453

    Source documentation

    A continuous-path version of the standard excursion; the fallback occurs only on a null set under the standing Brownian hypotheses.

    def standardExcursionPath {Ω : Type} (B : Fin 3 → ℝ≥0 → Ω → ℝ) (ω : Ω) :
        C(unitInterval, ℝ) := ContinuousMap.mkD (standardExcursion B ω) 0

    Mentions: OAI.FKCRT.standardExcursion

43. lemma OAI.FKCRT.standardExcursionPath_ae_eq line 456
44. lemma OAI.FKCRT.standardExcursion_eval_aemeasurable line 464
45. lemma OAI.FKCRT.continuousMap_dense_eval_measurableEmbedding line 477

    Source documentation

    Evaluation on a countable dense set recovers the Borel structure of the uniform topology. This avoids any unproved stochastic-process measurability.

    lemma continuousMap_dense_eval_measurableEmbedding :
        MeasurableEmbedding (fun f : C(unitInterval, ℝ) =>
          fun n : ℕ => f (TopologicalSpace.denseSeq unitInterval n)) := by
    …

46. lemma OAI.FKCRT.standardExcursionPath_aemeasurable line 490
47. lemma OAI.FKCRT.IsGHPTest.brownian_integrable line 501