OAI/Combinatorics/PlanarL1/BandTrees.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarL1.Columns.Model.BandTrees.band line 17
2. abbrev OAI.PlanarL1.Columns.Model.BandTrees.Component line 18
3. def OAI.PlanarL1.Columns.Model.BandTrees.root line 19
4. lemma OAI.PlanarL1.Columns.Model.BandTrees.root_mem line 20
5. def OAI.PlanarL1.Columns.Model.BandTrees.middle line 22
6. lemma OAI.PlanarL1.Columns.Model.BandTrees.middle_mem line 23
7. def OAI.PlanarL1.Columns.Model.BandTrees.point line 26
8. def OAI.PlanarL1.Columns.Model.BandTrees.base line 29
9. def OAI.PlanarL1.Columns.Model.BandTrees.tree line 31
10. lemma OAI.PlanarL1.Columns.Model.BandTrees.reachable_mem line 50
11. def OAI.PlanarL1.Columns.Model.BandTrees.levels line 58

    Source documentation

    Only the radial layers meeting a column occur. No infinite layer family or arbitrary cut-off is added to the finite random step.

    noncomputable def levels (C : Component M P lo) (phase width : ℝ) : Finset ℤ :=
    …

    Mentions: OAI.PlanarL1.Columns.Model.BandTrees.Component

12. lemma OAI.PlanarL1.Columns.Model.BandTrees.level_of_mem line 61
13. lemma OAI.PlanarL1.Columns.Model.BandTrees.same_level line 77
14. abbrev OAI.PlanarL1.Columns.Model.BandTrees.MainIndex line 92
15. instance OAI.PlanarL1.Columns.Model.BandTrees.(instance at line 95) line 95
16. def OAI.PlanarL1.Columns.Model.BandTrees.anchor line 98
17. lemma OAI.PlanarL1.Columns.Model.BandTrees.anchor_mem line 103
18. lemma OAI.PlanarL1.Columns.Model.BandTrees.same_component line 107
19. lemma OAI.PlanarL1.Columns.Model.BandTrees.main_disjoint line 117
20. lemma OAI.PlanarL1.Columns.Model.Path.restrict_of_length line 146

    Source documentation

    A short path stays in a height interval containing its entire permitted height deviation. This restricts the actual switching path, not a metric model.

    lemma restrict_of_length (p : M.Path I i j) (a b c t : ℝ)
        (hJ : ∀ H, |H-c|≤t → H ∈ J) (hp : |a-c|+p.length a b≤t) :
        ∃ q : M.Path J i j, q.length a b=p.length a b := by
    …

21. lemma OAI.PlanarL1.Columns.Model.Point.dist_coordinates line 163
22. lemma OAI.PlanarL1.Columns.Model.Point.local_point line 172

    Source documentation

    On a ball farther from the band ends than its radius, unrestricted shortest paths give exact intrinsic distances from its center.

    lemma local_point (x y : M.Point I r) (x' : M.Point J s)
        (hx : x'.column=x.column) (hX : x'.height=x.height)
        (hI : IsClosed I) (hJI : J ⊆ I) {t : ℝ}
        (hJ : ∀ H, |H-x.height|≤t → H ∈ J) (hxy : dist x y≤t) :
        ∃ y' : M.Point J s, y'.column=y.column ∧ y'.height=y.height ∧ dist x' y'=dist x y := by
    …

23. lemma OAI.PlanarL1.Columns.Model.Field.constant_ordered line 212
24. lemma OAI.PlanarL1.Columns.Model.OrdinaryData.support_at line 220

    Source documentation

    The support required by a secondary group is constructed from the actual old point source. The comparison outside that source's component is never used.

    lemma support_at (D : OrdinaryData M) (i : Fin (k+1)) (H : ℝ) (hi : D.Contains i H) :
        ∃ (F : M.Field D.band 1) (a b : Fin (k+1)), F.OrderedFrom a b ∧
          F.value i ⟨H,hi.1⟩=D.comparison.value i ⟨H,hi.1⟩ ∧
          ∀ (j : Fin (k+1)) (T : ℝ) (hj : D.Contains j T),
            F.value j ⟨T,hj.1⟩≤D.comparison.value j ⟨T,hj.1⟩ := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.OrdinaryData

25. lemma OAI.PlanarL1.Columns.Model.Ambient.coordinate_point line 250
26. lemma OAI.PlanarL1.Columns.Model.Ambient.point_dist_same line 254
27. def OAI.PlanarL1.Columns.Model.Ambient.Common line 259

    Source documentation

    A chart identifier is common on the actual unrestricted closed ball. The test includes every representative, not merely the original vertices.

    def Common {ι : Type*} (name : Fin (k+1) → ℝ → ι)
        (x : M.Point Set.univ A.root) (r : ℝ) (a : ι) : Prop :=
    …

28. lemma OAI.PlanarL1.Columns.Model.Ambient.Common.mono line 263
29. lemma OAI.PlanarL1.Columns.Model.Ambient.Common.center line 268
30. lemma OAI.PlanarL1.Columns.Model.Ambient.Common.shift line 273
31. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.ball_band line 287

    Source documentation

    Band containment follows from a common geometric ball and ordinary vertical segments, rather than being assumed in a secondary update.

    lemma ball_band {x : M.Point Set.univ A.root} {a : Fin (S.count+1)} {r : ℝ}
        (h : A.Common S.name x r a) {J : Set ℝ}
        (hJ : ∀ H ∈ J, |x.height-H|≤r) : J ⊆ (S.chart a).band := by
    …

32. lemma OAI.PlanarL1.Columns.Model.BState.height_named line 303
33. lemma OAI.PlanarL1.Columns.Model.BState.uses_named line 308
34. lemma OAI.PlanarL1.Columns.Model.BState.ball_band line 313