PairGeometry.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.PlanarL1.Columns.Model.Activity.terminal_certificate_circular line 12
lemma OAI.PlanarL1.Columns.Model.Activity.terminal_survival_circular line 27
lemma OAI.PlanarL1.Columns.Model.SetSystem.refinedMap_terminal_circular line 48
lemma OAI.PlanarL1.Columns.Model.SetSystem.refined_certificate_survival_circular line 79
def OAI.PlanarL1.Threshold.Variables.slab line 147
Source documentation
A literal half-sign label rectangle, pulled back through the actual old chart variables. No independence of different old charts is asserted.
```
noncomputable def slab (Z : Variables Ω μ) (b : Bool) (lo hi : ℝ) : Set Ω :=
…
```
Mentions: OAI.PlanarL1.Threshold.Variables
lemma OAI.PlanarL1.Threshold.Variables.measurable_slab line 149
lemma OAI.PlanarL1.Threshold.Variables.mem_slab line 152
lemma OAI.PlanarL1.Threshold.Variables.measure_slab line 155

lemma OAI.PlanarL1.Columns.Model.OrdinaryState.barrier_labels line 174

Source documentation

The elementary barrier rectangle in one literal ordinary chart. All three memberships and its uniform real mass are produced, rather than assumed.

lemma barrier_labels (a : Fin (S.count+1)) {root : Fin n}
    (x y e : M.Point (S.chart a).band root)
    (hx : S.name x.column x.height=a) (hy : S.name y.column y.height=a)
    (he : S.name e.column e.height=a)
    {lo : ℝ} (hxH : x.height ∈ Set.Icc lo (lo+a₂))
    (hyH : y.height ∈ Set.Icc lo (lo+a₂)) (heH : e.height ∈ Set.Icc lo (lo+a₂))
    (hclose : |(S.chart a).comparison.eval x-(S.chart a).comparison.eval y| ≤ EA)
    (hdrop : (S.chart a).comparison.eval e < (S.chart a).comparison.eval x-j ∨
      (S.chart a).comparison.eval e < (S.chart a).comparison.eval y-j) :
    ∃ E : Set Ω, MeasurableSet E ∧ kappaA*j/4 ≤ μ.real E ∧
      (∀ ω ∈ E, (S.sets.activity ω).active x.column x.height) ∧
      (∀ ω ∈ E, (S.sets.activity ω).active y.column y.height) ∧
…

lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.pair_distance_external line 281

Source documentation

The other endpoint can be in another broad component. Only its actual old identifier and its absence from this cell matter for the indicator calculation.

lemma pair_distance_external (x : M.Point J root) (j : Fin n) (T : ℝ)
    (hT : T ∈ U.data.band) (hx : x.column ∈ ColumnOrder.componentColumns U.cell)
    (hy : T ∉ MainCell.domain U.tree U.phase U.cell j) (hyn : S.name j T=U.index) :
    (∫ ω, |(U.patch.apply.activity ω).indicator x.column x.height-
        (U.patch.apply.activity ω).indicator j T| ∂(μ.prod Threshold.fair)) =
      max |x.height-T| (κ*|MainCell.replacement U.comparison U.sub_old U.tree U.phase U.cell
        U.anchor U.noise U.error U.shield_offset U.lo x-U.comparison.value j ⟨T,hT⟩|) := by
…

Mentions: OAI.PlanarL1.ColumnOrder.componentColumns, OAI.PlanarL1.Columns.Model.MainCell.domain, OAI.PlanarL1.Threshold.fair, OAI.PlanarL1.Columns.Model.MainCell.replacement

lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.separation_of_raise_external line 308
lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.pair_separation_external line 325