OAI/Combinatorics/PlanarL1/MainCells.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarL1.Columns.Model.Field.widen_lipschitz line 15
2. abbrev OAI.PlanarL1.Columns.Model.MainCell.Cell line 26
3. def OAI.PlanarL1.Columns.Model.MainCell.old line 29
4. def OAI.PlanarL1.Columns.Model.MainCell.boundary line 31
5. def OAI.PlanarL1.Columns.Model.MainCell.input line 34
6. def OAI.PlanarL1.Columns.Model.MainCell.proposal line 37
7. lemma OAI.PlanarL1.Columns.Model.MainCell.boundary_compact line 41
8. lemma OAI.PlanarL1.Columns.Model.MainCell.old_lipschitz line 45
9. lemma OAI.PlanarL1.Columns.Model.MainCell.input_lipschitz line 48
10. lemma OAI.PlanarL1.Columns.Model.MainCell.proposal_accuracy line 56
11. lemma OAI.PlanarL1.Columns.Model.MainCell.proposal_lipschitz line 66
12. lemma OAI.PlanarL1.Columns.Model.MainCell.frontier_margin line 72
13. lemma OAI.PlanarL1.Columns.Model.MainCell.variation line 82
14. lemma OAI.PlanarL1.Columns.Model.MainCell.movement line 92
15. lemma OAI.PlanarL1.Columns.Model.MainCell.raise_or_descent line 108

    Source documentation

    The literal main test: the proposal is the actual interpolated compact frontier envelope, and failure to raise constructs an attaining path in J.

    lemma raise_or_descent (hJ : IsCompact J) (v w : M.Point J root)
        (hv : v.column ∈ ColumnOrder.componentColumns C)
        (hw : w.column ∈ ColumnOrder.componentColumns C)
        {ε : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ (1:ℝ)/100)
        (hζ : R.ζ = ε/100) (hδ : R.δ = (ε/1000)/8)
        {α : Point.RadialTree.Noise (n := n)} (hα : R.NoiseBounds α)
    …

    Mentions: OAI.PlanarL1.ColumnOrder.componentColumns, OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

16. def OAI.PlanarL1.Columns.Model.MainCell.replacement line 179
17. def OAI.PlanarL1.Columns.Model.MainCell.replacementConstant line 184
18. lemma OAI.PlanarL1.Columns.Model.MainCell.replacement_lipschitz line 187
19. lemma OAI.PlanarL1.Columns.Model.MainCell.replacement_switch line 205
20. lemma OAI.PlanarL1.Columns.Model.MainCell.replacement_frontier line 215
21. lemma OAI.PlanarL1.Columns.Model.MainCell.replacement_endpoint line 225
22. lemma OAI.PlanarL1.Columns.Model.MainCell.scaled_replacement_constant line 242
23. def OAI.PlanarL1.Columns.Model.MainCell.domain line 254

    Source documentation

    Actual closed full-column update domain.

    def domain (i : Fin n) : Set ℝ :=
    …

24. lemma OAI.PlanarL1.Columns.Model.MainCell.mem_domain line 257
25. lemma OAI.PlanarL1.Columns.Model.MainCell.closed_domain line 261
26. def OAI.PlanarL1.Columns.Model.MainCell.cellPoint line 268

    Source documentation

    The actual point in the broad component underlying a cell-domain point.

    def cellPoint (i : Fin n) (H : ℝ) (h : H ∈ domain R q C i) : M.Point J root :=
    …

    Mentions: OAI.PlanarL1.Columns.Model.MainCell.domain

27. def OAI.PlanarL1.Columns.Model.MainCell.converted line 272
28. lemma OAI.PlanarL1.Columns.Model.MainCell.converted_on line 277
29. lemma OAI.PlanarL1.Columns.Model.MainCell.converted_lipschitz line 284
30. def OAI.PlanarL1.Columns.Model.MainCell.patch line 315

    Source documentation

    A kept main cell, with the literal interpolated proposal and trapezoidal shield, is an actual invariant-preserving measurable set update. The old chart agreement is used only on its real update domain.

    noncomputable def patch {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
        (A : SetSystem M Ω μ) (Z : Threshold.Variables Ω μ)
        (hJ : IsCompact J) (lo : ℝ) (hband : J = Icc lo (lo+R.a))
        (hthin : R.a ≤ (1/1000:ℝ)/1000)
        (v : M.Point J root) (hv : v.column ∈ ColumnOrder.componentColumns C)
        {α : Point.RadialTree.Noise (n := n)} (hα : R.NoiseBounds α)
    …

    Mentions: OAI.PlanarL1.Columns.Model.SetSystem, OAI.PlanarL1.Threshold.Variables, OAI.PlanarL1.ColumnOrder.componentColumns, OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

31. lemma OAI.PlanarL1.Columns.Model.Point.near_frontier_of_not_mem line 367

    Source documentation

    A shortest path leaving any full-column cell meets its actual frontier before using more than its total length. No shape/convexity of the cell is used.

    lemma near_frontier_of_not_mem (hJ : IsClosed J) (S : Set (Fin n))
        (x y : M.Point J root) (hx : x.column ∈ S) (hy : y.column ∉ S) :
        ∃ z : M.Point J root, z.column ∈ frontier (M := M) (J := J) S ∧ dist x z ≤ dist x y := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.Point.frontier

32. def OAI.PlanarL1.Columns.Model.MainCell.namedReplacement line 391
33. lemma OAI.PlanarL1.Columns.Model.MainCell.namedReplacement_value line 396
34. def OAI.PlanarL1.Columns.Model.MainCell.localClipAtom line 402
35. lemma OAI.PlanarL1.Columns.Model.MainCell.shield_lipschitz line 407
36. lemma OAI.PlanarL1.Columns.Model.MainCell.localClipAtom_lipschitz line 421
37. lemma OAI.PlanarL1.Columns.Model.MainCell.localClipPair_probability_lt line 435
38. lemma OAI.PlanarL1.Columns.Model.MainCell.localClipPair_probability line 505
39. lemma OAI.PlanarL1.Columns.Model.MainCell.namedReplacement_probability line 523

    Source documentation

    The main clipping part of chart persistence. This is for the literal interpolated, shifted, height-clipped proposal, including the old field's retaining branch and inherited names through interpolation layers.

    lemma namedReplacement_probability (hJ : IsCompact J) (v x : M.Point J root)
        (E lo B : ℝ) (hB : 0 < B) {ρ : ℝ} (hρ : 0 ≤ ρ) (hs : ρ ≤ R.radius)
        (m : ℕ) (hm : 0 < m) :
        FiniteRandom.prob (fun ω : Point.RadialTree.GridSample (n := n) R.depthCap m × Fin (m+1) =>
    …

    Mentions: OAI.PlanarL1.FiniteRandom.prob, OAI.PlanarL1.Columns.Model.Point.RadialTree.GridSample

40. lemma OAI.PlanarL1.Columns.Model.MainCell.namedReplacement_near_frontier line 588
41. lemma OAI.PlanarL1.Columns.Model.MainCell.namedReplacement_retained_on_touched_ball line 607

    Source documentation

    Crossing a main-cell boundary causes no identifier loss at all. This is exactly why no radial padding error proportional to the band width is needed in the source persistence bound.

    lemma namedReplacement_retained_on_touched_ball (hJ : IsCompact J)
        (v x : M.Point J root) {ρ : ℝ} {α : Point.RadialTree.Noise (n := n)}
    …

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

42. lemma OAI.PlanarL1.Columns.Model.MainCell.namedReplacement_cases line 639
43. lemma OAI.PlanarL1.Columns.Model.MainCell.namedReplacement_bound line 655
44. lemma OAI.PlanarL1.Columns.Model.MainCell.namedReplacement_congr_zero line 667
45. def OAI.PlanarL1.Columns.Model.MainCell.choose line 686

    Source documentation

    A local winner other than the old field receives exactly one new name. The height-only branch is zero in the fresh block, and spatial atom a is a+1.

    noncomputable def choose (v : M.Point J root)
        (α : Point.RadialTree.Noise (n := n)) (E β lo : ℝ) (i : Fin n) (H : ℝ) :
    …

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

46. lemma OAI.PlanarL1.Columns.Model.MainCell.choose_spec line 698
47. lemma OAI.PlanarL1.Columns.Model.MainCell.choose_none_inside line 714
48. lemma OAI.PlanarL1.Columns.Model.MainCell.choose_none_outside line 723
49. lemma OAI.PlanarL1.Columns.Model.MainCell.choose_none_frontier line 728
50. lemma OAI.PlanarL1.Columns.Model.MainCell.choose_switch line 741