OAI/Combinatorics/PlanarL1/MainPersistence.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.choose_eq line 15
2. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.name_eq line 24
3. lemma OAI.PlanarL1.Columns.Model.MainCell.choose_eq_of_name line 35
4. lemma OAI.PlanarL1.Columns.Model.MainCell.choose_none_of_name line 44
5. lemma OAI.PlanarL1.Tiling.near_band_unique line 60
6. lemma OAI.PlanarL1.Tiling.near_mem_band line 84
7. lemma OAI.PlanarL1.Columns.Model.Point.local_center line 99
8. lemma OAI.PlanarL1.Columns.Model.MainFamily.touched_band line 118
9. lemma OAI.PlanarL1.Columns.Model.MainFamily.touched_envelope line 125
10. lemma OAI.PlanarL1.Columns.Model.MainFamily.local_center line 136
11. lemma OAI.PlanarL1.Columns.Model.MainFamily.local_ball line 144
12. lemma OAI.PlanarL1.Columns.Model.Point.eq_of_coordinates line 174
13. lemma OAI.PlanarL1.Columns.Model.MainFamily.choose_none_crossed line 194

    Source documentation

    An actual available main cell does not install an identifier anywhere in a small padded ball if that ball has a column outside the cell.

    lemma choose_none_crossed (c : Kept A S phase omega)
        (hex : ∃ y : M.Point Set.univ A.root, dist x y≤ρ ∧
          y.column ∉ ColumnOrder.componentColumns c.val.2.2)
        (z : M.Point Set.univ A.root) (hz : dist x z≤ρ) :
        (keptStep A S phase hm omega c).choose z.column z.height=none := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.MainFamily.Kept, OAI.PlanarL1.ColumnOrder.componentColumns, OAI.PlanarL1.Columns.Model.MainFamily.keptStep

14. lemma OAI.PlanarL1.Columns.Model.MainFamily.all_choices_none_crossed line 229

    Source documentation

    If two main cells are seen by the center ball, every cell's chosen name is none on the ball. This also covers two representatives of the same quotient point and arbitrarily many touched cells.

    lemma all_choices_none_crossed (c : CellIndex q L U phase)
        (hc : x.height ∈ domain phase c x.column)
        (hex : ∃ y : M.Point Set.univ A.root, dist x y≤ρ ∧
          y.column ∉ ColumnOrder.componentColumns c.2.2)
        (z : M.Point Set.univ A.root) (hz : dist x z≤ρ)
        (d : Kept A S phase omega) :
        (keptStep A S phase hm omega d).choose z.column z.height=none := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.MainFamily.CellIndex, OAI.PlanarL1.Columns.Model.MainFamily.domain, OAI.PlanarL1.ColumnOrder.componentColumns, OAI.PlanarL1.Columns.Model.MainFamily.Kept, OAI.PlanarL1.Columns.Model.MainFamily.keptStep

15. lemma OAI.PlanarL1.FiniteRandom.prob_pi_eval_bound line 265
16. def OAI.PlanarL1.Columns.Model.MainFamily.sampleName line 294
17. lemma OAI.PlanarL1.Columns.Model.MainFamily.choose_none_other line 304
18. lemma OAI.PlanarL1.Columns.Model.MainFamily.result_name_eq line 317
19. def OAI.PlanarL1.Columns.Model.MainFamily.localLoss line 381
20. lemma OAI.PlanarL1.Columns.Model.MainFamily.localLoss_nonneg line 385
21. lemma OAI.PlanarL1.Columns.Model.MainFamily.sampleName_probability line 390
22. lemma OAI.PlanarL1.Columns.Model.MainFamily.persistence_probability line 412

    Source documentation

    Chart persistence for the whole literal main mode, conditional on the padded height band. No factor depending on the number of graph cells occurs.

    lemma persistence_probability [SFinite μ] (x : M.Point Set.univ A.root)
        (c : CellIndex q L U phase) (hc : x.height ∈ domain phase c x.column)
        {ρ : ℝ} (hρ : 0≤ρ) (hp : Tiling.Padded a₁ q x.height ρ)
        (hsmall : 4*ρ<3*EA) (hr : ρ≤(tree phase c).radius)
        (hold : ∀ z : M.Point Set.univ A.root, dist x z≤ρ →
          S.name z.column z.height=S.name x.column x.height)
        (m : ℕ) (hm : 0 < m) :
        prob (fun omega : Sample phase m => ∃ z : M.Point Set.univ A.root, dist x z≤ρ ∧
          (result A S phase hm omega).name z.column z.height≠
            (result A S phase hm omega).name x.column x.height) ≤ localLoss phase c ρ m := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.MainFamily.CellIndex, OAI.PlanarL1.Columns.Model.MainFamily.domain, OAI.PlanarL1.Tiling.Padded, OAI.PlanarL1.Columns.Model.MainFamily.tree, OAI.PlanarL1.Columns.Model.MainFamily.Sample, OAI.PlanarL1.Columns.Model.MainFamily.result, OAI.PlanarL1.Columns.Model.MainFamily.localLoss