OAI/Geometry/PinnedDistances/CutGeometry.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPinned.Hierarchy.Depth.allCuts line 43
2. lemma OAI.WeakPinned.Hierarchy.Depth.mem_allCuts line 47
3. lemma OAI.WeakPinned.Hierarchy.Depth.cells_subset_allCuts line 51
4. lemma OAI.WeakPinned.Hierarchy.Depth.allCuts_laminar line 54
5. def OAI.WeakPinned.Hierarchy.Depth.cutAt line 66
6. def OAI.WeakPinned.Hierarchy.Depth.cutLength line 69
7. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_cutAt line 71
8. lemma OAI.WeakPinned.Hierarchy.Depth.cutAt_bound line 74
9. lemma OAI.WeakPinned.Hierarchy.Depth.cutAt_vanish line 78
10. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_cutAt line 89
11. lemma OAI.WeakPinned.Hierarchy.Depth.cutLength_nonneg line 94
12. lemma OAI.WeakPinned.Hierarchy.Depth.cutLength_eq_zero line 103
13. lemma OAI.WeakPinned.Hierarchy.Depth.cutLength_outside line 106
14. lemma OAI.WeakPinned.Hierarchy.Depth.integral_cut_sum line 111
15. lemma OAI.WeakPinned.Hierarchy.Depth.symmetric_integral_cut_sum line 125
16. lemma OAI.WeakPinned.Hierarchy.Depth.cutLength_balanced line 135
17. lemma OAI.WeakPinned.Hierarchy.Depth.actual_cut_fluctuation line 143
18. lemma OAI.WeakPinned.Hierarchy.Depth.value_eq_of_lt line 160
19. def OAI.WeakPinned.Hierarchy.Depth.differenceTail line 170
20. lemma OAI.WeakPinned.Hierarchy.Depth.differenceTail_pos line 173
21. lemma OAI.WeakPinned.Hierarchy.Depth.differenceTail_neg_compl line 194
22. lemma OAI.WeakPinned.Hierarchy.Depth.mass_compl line 225
23. lemma OAI.WeakPinned.Hierarchy.Depth.ae_differenceTail_formula line 232
24. def OAI.WeakPinned.Hierarchy.Depth.aboveCell line 254
25. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_aboveCell line 258
26. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_aboveCell line 265
27. lemma OAI.WeakPinned.Hierarchy.Depth.sum_cut_separation line 281
28. lemma OAI.WeakPinned.Hierarchy.Depth.cut_distance_two_integrals line 318
29. lemma OAI.WeakPinned.Hierarchy.Depth.cut_projection line 336

    Source documentation

    Exact projection identity, including the formal infinite values at the two endpoints, represented by their tail-set membership.

    lemma cut_projection (p : P → ℝ) (hp : ∑ x, p x=1) (w : ℝ → ℝ)
        (hwu : w 1=0) (hws : ∀ x, w (p x)=0) (hwsym : ∀ u, w (1-u)=w u)
        (x y : P) (hxy : x ≠ y) :
        Cuts.distance d.allCuts (d.cutLength (fun C => w (Cuts.mass p C))) x y =
          ∫ u, w (Cuts.mass p (d.differenceTail x y u)) := by
    …

    Mentions: OAI.WeakPinned.Cuts.distance, OAI.WeakPinned.Cuts.mass

30. def OAI.WeakPinned.Tail.step line 364
31. def OAI.WeakPinned.Tail.law line 366
32. lemma OAI.WeakPinned.Tail.measurable_step line 368
33. lemma OAI.WeakPinned.Tail.measurable_law line 371
34. lemma OAI.WeakPinned.Tail.step_difference line 374
35. lemma OAI.WeakPinned.Tail.step_difference_indicator line 391
36. lemma OAI.WeakPinned.Tail.integrable_step_difference line 396
37. lemma OAI.WeakPinned.Tail.integral_step_difference line 400
38. lemma OAI.WeakPinned.Tail.law_difference_bound line 408
39. lemma OAI.WeakPinned.Tail.lipschitz_tail_bound line 418
40. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_cellWeight line 448
41. lemma OAI.WeakPinned.Hierarchy.Depth.cut_root_projection line 461
42. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_differenceTail line 480
43. def OAI.WeakPinned.Tail.offTwo line 502
44. lemma OAI.WeakPinned.Tail.offTwo_nonneg line 505
45. lemma OAI.WeakPinned.Tail.mass_as_sum line 509
46. lemma OAI.WeakPinned.Tail.differenceTail_law line 512
47. lemma OAI.WeakPinned.Tail.rootTail_law line 526
48. lemma OAI.WeakPinned.Tail.fiber_cut_error line 542

    Source documentation

    Quantitative fiber-tree comparison, before inserting the arithmetic raw-depth equation. The y endpoint is included; x has zero fiber mass.

    lemma fiber_cut_error (d d' : Depth P) (p : P → ℝ) (hp0 : ∀ z, 0 ≤ p z) (hp : ∑ z, p z=1)
        (w : ℝ → ℝ) (Λ : ℝ≥0) (hw : LipschitzWith Λ w)
        (hwu : w 1=0) (hws : ∀ z, w (p z)=0) (hwsym : ∀ u, w (1-u)=w u)
        (x y : P) (hpx : p x=0) (hxy : x ≠ y) (c : ℝ) :
        |Cuts.distance d.allCuts (d.cutLength (fun C => w (Cuts.mass p C))) x y-
          Cuts.rootDistance d'.allCuts (d'.cutLength (fun C => w (Cuts.mass p C))) y| ≤
          (Λ:ℝ)*∑ z, offTwo p x y z*|d.value y z-d.value x z-(d'.value y z+c)| := by
    …

    Mentions: OAI.WeakPinned.Cuts.distance, OAI.WeakPinned.Cuts.mass, OAI.WeakPinned.Cuts.rootDistance, OAI.WeakPinned.Tail.offTwo

49. lemma OAI.WeakPinned.Arithmetic.paired_log line 578
50. lemma OAI.WeakPinned.Arithmetic.absval_sub_symm line 591
51. lemma OAI.WeakPinned.Arithmetic.raw_cross_fiber line 596

    Source documentation

    The raw cross-fiber identity at every place. The three points are distinct and the source is outside its fiber.

    lemma raw_cross_fiber {P : Type u9} (Z₁ Z₂ : P → K) (h₁ : Function.Injective Z₁)
        (h₂ : Function.Injective Z₂) (v : AbsoluteValue K ℝ) (x y z : P)
        (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z) (t : K)
        (hy : (Z₁ x-Z₁ y)*(Z₂ x-Z₂ y)=t)
        (hz : (Z₁ x-Z₁ z)*(Z₂ x-Z₂ z)=t) :
        -Real.log (v (Z₂ y-Z₂ z)) = -Real.log (v (Z₁ y-Z₁ z))-
          (-Real.log (v (Z₁ x-Z₁ z)))-Real.log (v t)-(-Real.log (v (Z₁ x-Z₁ y))) := by
    …