OAI/Geometry/PinnedDistances/SmallCells.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPinned.Hierarchy.Depth.sourceGiant line 29
2. instance OAI.WeakPinned.Hierarchy.Depth.(instance at line 30) line 30
3. lemma OAI.WeakPinned.Hierarchy.Depth.sourceGiant_mono line 33
4. lemma OAI.WeakPinned.Hierarchy.Depth.sourceGiant_iff line 41
5. lemma OAI.WeakPinned.Hierarchy.Depth.isClosed_sourceGiant line 52
6. def OAI.WeakPinned.Hierarchy.Depth.sourceM line 70
7. lemma OAI.WeakPinned.Hierarchy.Depth.sourceGiant_cutoff line 72
8. lemma OAI.WeakPinned.Hierarchy.Depth.sourceM_le_M line 89
9. lemma OAI.WeakPinned.Hierarchy.Depth.sourceGiant_mem_giant line 95
10. lemma OAI.WeakPinned.Hierarchy.Depth.outsideIndicator_source line 107
11. lemma OAI.WeakPinned.Hierarchy.Depth.potential_source line 117
12. lemma OAI.WeakPinned.Hierarchy.Depth.straddle_integral line 131

    Source documentation

    The level set is an interval of length 2H, regardless of the fiber center-level h.

    lemma straddle_integral (hn : 2 ≤ Fintype.card P) (x : P) (h H : ℝ) (hH : 0 ≤ H) :
        (∫ r : ℝ, if d.sourceGiant x (h-r-H) ∧ ¬d.sourceGiant x (h-r+H) then (1:ℝ) else 0) = 2*H := by
    …

13. def OAI.WeakPinned.Hierarchy.Depth.smallCells line 147
14. def OAI.WeakPinned.Hierarchy.Depth.smallNeighbors line 151
15. lemma OAI.WeakPinned.Hierarchy.Depth.smallCells_chain line 154
16. lemma OAI.WeakPinned.Hierarchy.Depth.smallNeighbors_card line 163
17. lemma OAI.WeakPinned.Hierarchy.Depth.source_mem_smallNeighbors line 186
18. lemma OAI.WeakPinned.Hierarchy.Depth.smallNeighbors_self line 202
19. lemma OAI.WeakPinned.Hierarchy.Depth.smallNeighbors_erase_bound line 211
20. lemma OAI.WeakPinned.Hierarchy.Depth.smallNeighbors_pair_bound line 231

    Source documentation

    All candidate sources for each target lie in one small neighborhood, allowing a level-dependent fiber reparametrization.

    lemma smallNeighbors_pair_bound (hn : 2 ≤ Fintype.card P)
        (q : P → P → ℝ) (B τ : ℝ) (hB : 0 ≤ B) (hτ : 0 < τ) (hτ1 : τ ≤ 1)
        (hq : ∀ x y, x ≠ y → q x y ≤ B / ((Fintype.card P : ℝ)*((Fintype.card P : ℝ)-1)))
        (C : Finset P) :
        (∑ y ∈ C, ∑ x ∈ (d.smallNeighbors y (τ*Fintype.card P)).erase y, q x y) ≤
          B*τ*((C.card : ℝ)/Fintype.card P) := by
    …

    Mentions: OAI.WeakPinned.B

21. def OAI.WeakPinned.SmallFiber.mass line 269

    Source documentation

    Probability of a finite subset; the fiber weights used below will be the exact uniform probabilities on the original retained distance fibers.

    def mass (p : P → ℝ) (C : Finset P) : ℝ := ∑ y ∈ C, p y
    …

22. lemma OAI.WeakPinned.SmallFiber.mass_nonneg line 272
23. lemma OAI.WeakPinned.SmallFiber.mass_mono line 276
24. lemma OAI.WeakPinned.SmallFiber.mass_le_one line 280
25. lemma OAI.WeakPinned.SmallFiber.mass_diff_inter line 284
26. lemma OAI.WeakPinned.SmallFiber.mass_cover line 293
27. lemma OAI.WeakPinned.SmallFiber.small_case_one line 303
28. lemma OAI.WeakPinned.Hierarchy.Depth.nongiant_share_overlap line 322
29. lemma OAI.WeakPinned.SmallFiber.mass_as_sum line 344
30. lemma OAI.WeakPinned.SmallFiber.mass_as_sum_off line 349
31. lemma OAI.WeakPinned.SmallFiber.nongiant_mass_bound line 359
32. lemma OAI.WeakPinned.SmallFiber.integral_open_interval line 376
33. lemma OAI.WeakPinned.SmallFiber.integral_closed_interval line 384
34. lemma OAI.WeakPinned.SmallFiber.integrable_open_interval line 392
35. lemma OAI.WeakPinned.SmallFiber.integrable_closed_interval line 400
36. def OAI.WeakPinned.SmallFiber.minusError line 408
37. def OAI.WeakPinned.SmallFiber.plusError line 411
38. lemma OAI.WeakPinned.SmallFiber.minusError_formula line 414
39. lemma OAI.WeakPinned.SmallFiber.plusError_formula line 430
40. lemma OAI.WeakPinned.SmallFiber.minusError_integrable line 446
41. lemma OAI.WeakPinned.SmallFiber.plusError_integrable line 452
42. lemma OAI.WeakPinned.SmallFiber.minusError_integral line 458
43. lemma OAI.WeakPinned.SmallFiber.plusError_integral line 468
44. lemma OAI.WeakPinned.SmallFiber.two_truncations line 478
45. lemma OAI.WeakPinned.SmallFiber.errors_integral line 484
46. def OAI.WeakPinned.SmallFiber.activeMass line 502

    Source documentation

    Actual source cell, not a giant-complement occurrence.

    def activeMass (d : Depth P) (p : P → ℝ) (x : P) (T lam r : ℝ) : ℝ := by
    …

47. def OAI.WeakPinned.SmallFiber.nongiantMass line 507
48. def OAI.WeakPinned.SmallFiber.straddle line 510
49. def OAI.WeakPinned.SmallFiber.neighborMass line 513
50. lemma OAI.WeakPinned.SmallFiber.neighborMass_nonneg line 517
51. lemma OAI.WeakPinned.SmallFiber.nongiantMass_nonneg line 523
52. lemma OAI.WeakPinned.SmallFiber.case_three_bound line 528
53. lemma OAI.WeakPinned.SmallFiber.active_pointwise line 551

    Source documentation

    The pointwise small-fiber bound. The only independent error is the exact pair of intervals already evaluated.

    lemma active_pointwise (d d' : Depth P) (p : P → ℝ) (hp : ∀ y, 0 ≤ p y)
        (h1 : ∑ y, p y = 1) (x : P) (hx : p x = 0) (h H T lam r : ℝ)
        (hlam : 0 ≤ lam) (hlam2 : lam ≤ 1/2) :
        activeMass d p x T lam r ≤
          2*lam*nongiantMass d' p x (h-r-H) + lam*straddle d' x h H r +
          minusError d d' p x h H r + plusError d d' p x h H r +
          neighborMass d d' p x T (h-r+H) := by
    …

    Mentions: OAI.WeakPinned.SmallFiber.activeMass, OAI.WeakPinned.SmallFiber.nongiantMass, OAI.WeakPinned.SmallFiber.straddle, OAI.WeakPinned.SmallFiber.minusError, OAI.WeakPinned.SmallFiber.plusError, OAI.WeakPinned.SmallFiber.neighborMass

54. lemma OAI.WeakPinned.SmallFiber.nongiantMass_measurable line 585
55. lemma OAI.WeakPinned.SmallFiber.activeMass_measurable line 599
56. lemma OAI.WeakPinned.SmallFiber.nongiantMass_integrable line 614
57. lemma OAI.WeakPinned.SmallFiber.activeMass_integrable line 639
58. lemma OAI.WeakPinned.SmallFiber.straddle_integrable line 649
59. lemma OAI.WeakPinned.SmallFiber.neighborMass_integrable line 662
60. lemma OAI.WeakPinned.SmallFiber.neighborMass_integral line 674
61. lemma OAI.WeakPinned.SmallFiber.pairMass_integrable line 699
62. lemma OAI.WeakPinned.SmallFiber.integral_nongiantMass_bound line 708
63. lemma OAI.WeakPinned.SmallFiber.active_integral line 726

    Source documentation

    The local small-fiber bound for two entire realized hierarchies. This includes the exact signed-depth error; it will vanish at finite places and have an exponentially small grid mean at archimedean places.

    lemma active_integral (d d' : Depth P) (hn : 2 ≤ Fintype.card P)
        (p : P → ℝ) (hp : ∀ y, 0 ≤ p y) (h1 : ∑ y, p y = 1)
        (x : P) (hx : p x = 0) (h H T lam : ℝ)
        (hH : 0 ≤ H) (hlam : 0 ≤ lam) (hlam2 : lam ≤ 1/2) :
        (∫ r, activeMass d p x T lam r) ≤
          2*lam*(∑ y, p y * ∫ r, d'.pairOverlap r x y) + 2*lam*H +
          (∑ y, p y * max (|d.value x y+d'.value x y-h|-H) 0) +
          ∑ y, p y * (if x ∈ (d.smallNeighbors y T).erase y then d'.potential y else 0) := by
    …

    Mentions: OAI.WeakPinned.SmallFiber.activeMass

64. def OAI.WeakPinned.SmallFiber.edgeLaw line 769

    Source documentation

    Exact edge law induced by fiber sampling; no independence of fiber labels or levels is postulated.

    def edgeLaw {I : Type u8} [Fintype I] (w : I → ℝ) (p : I → P → ℝ) (x : I → P) (a b : P) : ℝ :=
    …

65. lemma OAI.WeakPinned.SmallFiber.fiber_neighbor_bound line 772