OAI/Combinatorics/PlanarL1/LocalPersistence.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarL1.Columns.Model.SecondaryCell.namedReplacement_eq_old_of_value line 15
2. lemma OAI.PlanarL1.Columns.Model.SecondaryCell.namedReplacement_boundary_ball line 22
3. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.chosen_name line 46
4. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.newIndex_names_injective line 51
5. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.chosen_iff_name line 61
6. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.choose_eq_of_name line 70
7. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.choose_none_of_old_name line 78
8. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.choose_eq line 87
9. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.name_eq line 95
10. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.name_eq_of_selected line 100
11. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.Block.eq_of_path_small line 129

    Source documentation

    At a doubly height-interior point, a narrow-band path can reach a seed only in this very processed broad/component/narrow block.

    lemma eq_of_path_small (d : Block (M := M) q p L U)
    …

    Mentions: OAI.PlanarL1.Columns.Model.RetainedSelection.Block

12. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.touch_block_small line 185
13. def OAI.PlanarL1.Columns.Model.RetainedSelection.localHit_small line 190
14. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.localHit_injective_small line 198
15. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.touching_card_small line 214

    Source documentation

    Universal packing for the whole actual, finitely selected family. Both old identifiers are derived by the local packing theorem, not assumed.

    lemma touching_card_small : Fintype.card (Hits A SA SB v hv b c (phaseD := phaseD) (phaseG := phaseG))≤
    …

    Mentions: OAI.PlanarL1.Columns.Model.RetainedSelection.Hits

16. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.touching_finset_card_small line 223
17. lemma OAI.PlanarL1.FiniteRandom.prob_update_bound_pi line 238
18. lemma OAI.PlanarL1.Interpolation.familyAtomPair_probability_pi line 257
19. lemma OAI.PlanarL1.Interpolation.familyNames_card_sparse line 310
20. lemma OAI.PlanarL1.Interpolation.selection_near_tie_modulus line 331
21. lemma OAI.PlanarL1.Interpolation.selection_probability_modulus line 347
22. lemma OAI.PlanarL1.Interpolation.maxSelection_modulus line 360
23. lemma OAI.PlanarL1.Interpolation.familySelection_modulus line 372
24. lemma OAI.PlanarL1.Interpolation.familyAtom_modulus line 381
25. lemma OAI.PlanarL1.Interpolation.familySelection_probability_sparse line 393

    Source documentation

    Sparse, genuinely independent component samples in the literal maximum. The full family numbering is retained even for groups irrelevant to the ball.

    lemma familySelection_probability_sparse {X I : Type*} {D : I → Type*}
        [Fintype I] [DecidableEq I] [∀ i, Fintype (D i)] [∀ i, Nonempty (D i)]
        {k N B : ℕ} (ι : Fin k → I) (hinj : Function.Injective ι)
        (old : X → ℝ) (F : ∀ g : Fin k, D (ι g) → X → NamedValue)
        (A : ∀ g : Fin k, D (ι g) → ℕ → X → ℝ)
        (S : Fin k → Finset ℕ) (T : Finset (Fin k))
        (hcard : ∀ g∈T, (S g).card≤N) (hout : ∀ g, g∉T → S g⊆{0}) (hT : T.card≤B)
        (x : X) (P : X → Prop) (hx : P x) {e b : ℝ} (hb : 0≤b)
        (ho : ∀ z, P z → |old x-old z|≤e)
        (hF : ∀ g ω z, P z → |(F g ω x).value-(F g ω z).value|≤e)
        (hA : ∀ g ω i z, P z → |A g ω i z-A g ω i x|≤e)
        (hzero : ∀ g ω z, A g ω 0 z=old z)
    …

    Mentions: OAI.PlanarL1.Interpolation.NamedValue

26. structure OAI.PlanarL1.Interpolation.LocalList line 435

    Source documentation

    A local finite atom expansion, including its proved one-coordinate tests. This is proof data for an actual named field, not a substitute for a chart.

    structure LocalList {X W : Type*} [Fintype W] (old : X → ℝ)
        (F : W → X → NamedValue) (x : X) (e b : ℝ) where
    …

    Mentions: OAI.PlanarL1.Interpolation.NamedValue

27. def OAI.PlanarL1.Interpolation.oldLocalList line 448
28. lemma OAI.PlanarL1.Interpolation.LocalList.family_probability line 460
29. lemma OAI.PlanarL1.Columns.Model.SecondaryCell.sampled_local_list line 486

    Source documentation

    Literal secondary field has a bounded local atom expansion on any lifted ball. The chosen radial node and the whole list precede all fresh offsets.

    lemma sampled_local_list {X : Type*} (lift : X → M.Point J root) (x : X) {ρ : ℝ}
        (hρ : 0≤ρ) (hs : ρ≤R.radius) (hd : ∀ z, dist (lift x) (lift z)≤ρ)
        (ordinary : Bool) (hOld : LipschitzWith 5 old) (hL : LipschitzWith 1 L)
        (hζ : R.ζ=(1:ℝ)/10) (pc radius lo B : ℝ) (hB : 0 < B) (m : ℕ) (hm : 0 < m) :
        ∃ C : LocalList (fun z => old (lift z))
          (fun (w : Point.RadialTree.GridSample (n := n) R.depthCap m × Fin (m+1) × Fin (m+1)) z =>
    …

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