SecondaryBatch.lean`

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.PlanarL1.Columns.Model.BState.SecondaryBatch line 18
Source documentation
All kept groups with one old identifier and one common orientation. Their closed domains may overlap in regions where several clippings act.
```
structure SecondaryBatch (S : BState M κ lam Ω μ) where
…
```
Mentions: OAI.PlanarL1.Columns.Model.BState
def OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.data line 34
def OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.comparison line 35
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.step_data line 37
def OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.groupHeight line 40
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.step_comparison line 43
def OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.groupNamed line 55
def OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.selected line 59
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.groupNamed_value line 62
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.comparison_scaled line 66
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.groupNamed_vertical line 79
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.selected_vertical line 86
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.groupNamed_switch line 90
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.selected_switch line 95
def OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.domain line 109
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.mem_domain line 112
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.domain_closed line 115
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.domain_band line 119
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.domain_name line 124
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.domain_switch line 128
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.group_frontier line 133
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.selected_same line 141
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.selected_frontier line 150
def OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.converted line 164
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.converted_on line 167
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.converted_vertical line 170
def OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.patch line 179
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.selected_cases line 201
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.selected_zero line 210
abbrev OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.NewIndex line 222
instance OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.(instance at line 223) line 223
def OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.chosen line 225
def OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.choose line 229
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.choose_some line 232
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.none_no_chosen line 239
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.exists_chosen line 245
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.chosen_switch line 263
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.choose_switch line 271
def OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.newData line 277
def OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.newLabels line 278
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.chosen_domain line 281
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.converted_chosen line 290
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.chosen_agreement line 314
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.chosen_description line 325
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.unchosen line 336
def OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.apply line 360
Source documentation
Literal finite maximum of overlapping secondary proposals, with the exact winning chart table and label variables. No sum over group movements is used.
```
noncomputable def apply [SFinite μ] : BState M κ lam (Ω × Bool) (μ.prod Threshold.fair) := by
…
```
Mentions: OAI.PlanarL1.Columns.Model.BState, OAI.PlanarL1.Threshold.fair
structure OAI.PlanarL1.Columns.Model.BState.SecondaryLayer line 394
Source documentation
The simultaneous secondary update, grouped by its actual old identifier. Within an identifier we take a maximum, not disjoint patching. Distinct old identifiers have disjoint domains because the old chart name is a function.
```
structure SecondaryLayer (S : BState M κ lam Ω μ) where
…
```
Mentions: OAI.PlanarL1.Columns.Model.BState
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.overlap line 401
abbrev OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.NewIndex line 409
instance OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.(instance at line 410) line 410
def OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.newData line 412
def OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.newLabels line 413
def OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.chosen line 416
def OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.choose line 419
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.choose_some line 422
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.choose_none line 429
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.choose_switch line 437
def OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.sets line 445
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.chosen_description line 448
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.unchosen line 462
def OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.apply line 470
Source documentation
The actual simultaneous layer and selected ordinary/ordered chart table.
```
noncomputable def apply [SFinite μ] : BState M κ lam (Ω × Bool) (μ.prod Threshold.fair) := by
…
```
Mentions: OAI.PlanarL1.Columns.Model.BState, OAI.PlanarL1.Threshold.fair