SecondaryGain.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.PlanarL1.Columns.Model.RetainedSelection.Block.broad_eq line 13
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.Block.narrow_eq line 18
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.Block.eq_of_path line 26
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 (d : Block (M := M) q p L U)
…
```
Mentions: OAI.PlanarL1.Columns.Model.RetainedSelection.Block
def OAI.PlanarL1.Columns.Model.RetainedSelection.Touch line 84
Source documentation
All actual processed groups that can affect this point through their narrow-band geometry. It is not just the groups having a prescribed ID.
```
def Touch (i : GroupIndex A SA SB v hv (p := p) (phaseD := phaseD) (phaseG := phaseG)) : Prop :=
…
```
Mentions: OAI.PlanarL1.Columns.Model.RetainedSelection.GroupIndex
abbrev OAI.PlanarL1.Columns.Model.RetainedSelection.Hits line 89
instance OAI.PlanarL1.Columns.Model.RetainedSelection.(instance at line 91) line 91
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.touch_block line 98
def OAI.PlanarL1.Columns.Model.RetainedSelection.localHit line 103
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.localHit_injective line 111
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.touching_card line 127
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 : Fintype.card (Hits A SA SB v hv b c (phaseD := phaseD) (phaseG := phaseG))≤
…
```
Mentions: OAI.PlanarL1.Columns.Model.RetainedSelection.Hits
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.touching_finset_card line 136
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.seed_domain line 157
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.seed_cellPoint line 164
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.step_gain line 178
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.full_step_gain line 193
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.domain_near line 228
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.domain_touch line 266

lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.far_not_domain line 295

Source documentation

A whole secondary group, not only the selected narrow component, stays away from the other endpoint of a distance-scale pair.

lemma far_not_domain (x : M.Point G.broad G.broad_root) (hx : x ∈ G.seeds)
    (j : Fin (k+1)) (T : ℝ) (hfar : 1 ≤ dist (A.point x.column x.height) (A.point j T))
    (positive : Bool) (C : G.Component) (hC : (G.admittedSeeds positive C).Nonempty) :
    T ∉ SecondaryCell.domain (G.admittedSeeds positive C) R j := by
…

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

lemma OAI.PlanarL1.Interpolation.maxSelection_ge_member line 323
lemma OAI.PlanarL1.Interpolation.familySelection_ge line 333
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.selected_ge line 351
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.indicator_inside line 356
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.indicator_outside line 362
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.pair_separation_external line 376

lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.gain_external line 393

Source documentation

Overlapping proposals at the raised endpoint can only help. It is enough for the other endpoint to stay outside all acting domains of its identifier.

lemma gain_external (q : Fin B.count) (i j : Fin (k+1)) (H T : ℝ)
    (hx : H ∈ SecondaryCell.domain (B.step q).seeds (B.step q).radius i)
    (hT : T ∈ B.data.band) (hy : T ∉ B.domain j) (hn : S.name j T=B.index)
    {r : ℝ} (hr : 0 < r) (hk : 0 < κ)
    (hclose : |B.comparison.value i ⟨H,B.domain_band (B.mem_domain.mpr ⟨q,hx⟩)⟩-
      B.comparison.value j ⟨T,hT⟩| ≤ r/10000)
    (hgain : (B.step q).comparison.value i
        (B.groupHeight q ⟨H,B.domain_band (B.mem_domain.mpr ⟨q,hx⟩)⟩)+r/25 <
      (B.step q).fullReplacement i
        (B.groupHeight q ⟨H,B.domain_band (B.mem_domain.mpr ⟨q,hx⟩)⟩)) :
    κ*r/50 < B.patch.apply.separation i H j T := by
…

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

lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.inside line 429
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.outside line 434
lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.pair_external line 447
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.actingStep_gain line 474
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.gain_external line 487
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.batch_not_domain line 549
lemma OAI.PlanarL1.FiniteRandom.prob_mono_instances line 586
lemma OAI.PlanarL1.FiniteRandom.prob_true line 591
lemma OAI.PlanarL1.FiniteRandom.prob_first line 594
lemma OAI.PlanarL1.FiniteRandom.prob_rectangle line 599
lemma OAI.PlanarL1.FiniteRandom.prob_coin line 611
lemma OAI.PlanarL1.FiniteRandom.prob_keep_outside line 615
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.prob_orientation_coins line 634
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.prob_orient_keep_suppress line 644