SecondaryFamily.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.PlanarL1.Columns.Model.BData.support_at line 19

Source documentation

A proved ordered support at the actual representative of a group. The support is needed only in an ordinary chart; ordered charts use their literal sphere admission test instead.

lemma support_at (D : BData M) (lam : ℝ≥0) (hlam : lam≤(1:ℝ≥0)/100)
    (positive : Bool) (i : Fin (k+1)) (H : ℝ) (hi : H ∈ D.band) (hu : D.Uses i) :
    ∃ (F : M.Field D.band 1) (a b : Fin (k+1)), F.OrderedFrom a b ∧
      (D.isOrdinary=true → F.value i ⟨H,hi⟩=(D.comparison lam hlam positive).value i ⟨H,hi⟩) ∧
      ∀ (j : Fin (k+1)) (T : D.band), D.isOrdinary=true → D.Uses j →
        F.value j T≤(D.comparison lam hlam positive).value j T := by
…

Mentions: OAI.PlanarL1.Columns.Model.BData, OAI.PlanarL1.Columns.Model.BData.value

lemma OAI.PlanarL1.Columns.Model.BData.uses_reachable line 35
structure OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group line 50
Source documentation
The geometric information attached to one actual surviving g-cell group. The seed collection is finite, lies in one broad component and one narrow height band, and keeps its TWO chart identifiers through the surviving-pair selection. The B half needed for its literal update is recorded here.
```
structure Group where
…
```
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.representative line 66
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.representative_mem line 67
abbrev OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.data line 68
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.lam line 69
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.lam_bound line 70
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.comparison line 73
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.value line 75
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.pc line 77
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.representative_uses line 79
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.value_lipschitz line 83
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.value_near line 86
abbrev OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.Component line 94
abbrev OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.root line 95
abbrev OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.tree line 96
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.inComponent line 98
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.narrowPoint line 101
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.allSeeds line 106
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.allSeeds_description line 109
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.old line 125
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.Admitted line 131
Source documentation
Literal admission; every ordinary seed is kept, and in an ordered chart this tests all points on the intrinsic narrow-band sphere.
```
def Admitted (positive : Bool) (C : G.Component)
    (w : M.Point (BandTrees.band narrow G.lower) (G.root C)) : Prop :=
…
```
Mentions: OAI.PlanarL1.Columns.Model.BandTrees.band
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.admittedSeeds line 136
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.admitted_sphere line 139
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.ordinary_admits line 146
structure OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.Support line 170
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.support line 180
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.old_eq line 186
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.seed_common line 193
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.component_uses line 199
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.seed_near line 207
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.support_seed_near line 214
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.domain_name line 233
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.step line 249
Source documentation
A nonempty admitted component now produces the literal, fully proved secondary clipping operation. No admission, support, name-gluing or movement conclusion is added as an assumption of the step.
```
noncomputable def step (positive : Bool) (C : G.Component)
    (hC : (G.admittedSeeds positive C).Nonempty)
    (noise : Point.RadialTree.Noise (n := k+1)) (hn : (G.tree C).NoiseBounds noise)
…
```
Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise
abbrev OAI.PlanarL1.Columns.Model.SecondaryGeometry.ComponentSample line 307
Source documentation
Offsets are fresh for each narrow component. The keep coin, by contrast, is shared by all the components of one surviving group.
```
abbrev ComponentSample (i : I) (C : (G i).Component) (m : ℕ) :=
…
```
Mentions: OAI.PlanarL1.Columns.Model.Component
abbrev OAI.PlanarL1.Columns.Model.SecondaryGeometry.Sample line 309
instance OAI.PlanarL1.Columns.Model.SecondaryGeometry.(instance at line 311) line 311
instance OAI.PlanarL1.Columns.Model.SecondaryGeometry.(instance at line 312) line 312
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.kept line 316
abbrev OAI.PlanarL1.Columns.Model.SecondaryGeometry.Acting line 317
instance OAI.PlanarL1.Columns.Model.SecondaryGeometry.(instance at line 320) line 320
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.offset_bound line 323
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.actingStep line 330
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.batch line 341
Source documentation
Literal maximum within an old B identifier. Neither disjoint domains nor an assumed winning branch replaces the actual overlapping maximum.
```
noncomputable def batch (a : Fin (S.count+1)) : BState.SecondaryBatch S where
…
```
Mentions: OAI.PlanarL1.Columns.Model.BState.SecondaryBatch
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.layer line 356
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.result line 360
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.execution line 366
Source documentation
Sampling all orientations, group coins, interpolation atoms and branches is a finite execution determined from the old geometric groups.
```
noncomputable def execution [SFinite μ] :
    Execution (BState M kappaB Group.lam (Ω × Bool) (μ.prod Threshold.fair)) :=
…
```
Mentions: OAI.PlanarL1.Execution, OAI.PlanarL1.Columns.Model.BState, OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.lam, OAI.PlanarL1.Threshold.fair