SecondaryCells.lean`

60 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PlanarL1.Columns.Model.SecondaryCell.seedDistance line 15
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.seedDistance_nonneg line 17
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.seedDistance_lipschitz line 19
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.seedDistance_seed line 21
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.seedDistance_attained line 24
def OAI.PlanarL1.Columns.Model.SecondaryCell.input line 28
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.input_lipschitz line 30
def OAI.PlanarL1.Columns.Model.SecondaryCell.approx line 38
def OAI.PlanarL1.Columns.Model.SecondaryCell.shallow line 41
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.approx_accuracy line 44
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.shallow_lipschitz line 54
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.shallow_boundary line 60
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.shallow_cap line 68
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.shallow_seed line 75
lemma OAI.PlanarL1.Columns.Model.Point.height_lipschitz line 95
def OAI.PlanarL1.Columns.Model.SecondaryCell.domain line 110
Source documentation
The literal closed union of radius-R seed balls, on each vertical column.
```
def domain (i : Fin n) : Set ℝ :=
…
```
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.mem_domain line 114
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.compact_domain line 122
def OAI.PlanarL1.Columns.Model.SecondaryCell.point line 129
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.point_column line 132
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.point_height line 134
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.point_distance line 136
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.inBand_of_mem line 139
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.equal_radius_or_endpoint line 143
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.switch_mem line 195
Source documentation
The seed-ball domain is saturated under the actual quotient switches.
```
lemma switch_mem {i j : Fin n} {H : ℝ} (hs : H ∈ M.heights i j)
    (hi : H ∈ domain S radius i) : H ∈ domain S radius j := by
…
```
Mentions: OAI.PlanarL1.Columns.Model.SecondaryCell.domain
def OAI.PlanarL1.Columns.Model.SecondaryCell.spatial line 229
def OAI.PlanarL1.Columns.Model.SecondaryCell.replacement line 234
def OAI.PlanarL1.Columns.Model.SecondaryCell.replacementConstant line 239
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.spatial_lipschitz line 241
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.replacement_lipschitz line 262
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.replacement_near line 280
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.spatial_boundary line 292
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.replacement_boundary line 310
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.replacement_endpoint line 321
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.scaled_replacement_constant line 337
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.point_dist line 348
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.point_dist_switch line 354
def OAI.PlanarL1.Columns.Model.SecondaryCell.converted line 362
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.converted_on line 367
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.converted_lipschitz line 373

def OAI.PlanarL1.Columns.Model.SecondaryCell.patch line 401

Source documentation

Literal secondary clipping on the actual closed seed-ball union, in both ordinary and admitted ordered orientations, is an invariant-preserving patch.

noncomputable def patch {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
    (A : SetSystem M Ω μ) (Z : Threshold.Variables Ω μ)
    (hJ : IsCompact J) (lo : ℝ) (hband : J = Icc lo (lo+R.a))
    (hS : S.Nonempty) (hOld : LipschitzWith 5 old) (hL : LipschitzWith 1 L)
    (hζ : R.ζ = (1:ℝ)/10) (pc radius αo αh c η κ : ℝ)
    (hr : 0 ≤ radius) (hrsmall : radius ≤ (1:ℝ)/100) (hαo : αo ≤ radius/1000)
    (hαh : αh ≤ radius/1000) (hδ : R.δ = (radius/1000)/8)
    {α : Point.RadialTree.Noise (n := n)} (hα : R.NoiseBounds α)
…

Mentions: OAI.PlanarL1.Columns.Model.SetSystem, OAI.PlanarL1.Threshold.Variables, OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

lemma OAI.PlanarL1.Columns.Model.SecondaryCell.replacement_seed line 441
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.replacement_movement line 458
def OAI.PlanarL1.Columns.Model.SecondaryCell.namedReplacement line 494
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.namedReplacement_value line 500
def OAI.PlanarL1.Columns.Model.SecondaryCell.localAtom line 507
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.orderedBranch_lipschitz line 513
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.shield_lipschitz line 524
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.localAtom_lipschitz line 538
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.localAtomPair_probability_lt line 554
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.localAtomPair_probability line 678

lemma OAI.PlanarL1.Columns.Model.SecondaryCell.namedReplacement_probability line 694

Source documentation

Literal secondary proposal with all spatial, ordered and height branches. The common atom list is determined before the fresh clipping parameters.

lemma namedReplacement_probability (hOld : LipschitzWith 5 old) (hL : LipschitzWith 1 L)
    (hζ : R.ζ = (1:ℝ)/10) (x : M.Point J root)
    (pc radius lo B : ℝ) (hB : 0 < B) {ρ : ℝ} (hρ : 0 ≤ ρ) (hs : ρ ≤ R.radius)
    (m : ℕ) (hm : 0 < m) :
    FiniteRandom.prob (fun ω : Point.RadialTree.GridSample (n := n) R.depthCap m × (Fin (m+1) × Fin (m+1)) =>
…

Mentions: OAI.PlanarL1.FiniteRandom.prob, OAI.PlanarL1.Columns.Model.Point.RadialTree.GridSample

lemma OAI.PlanarL1.Columns.Model.SecondaryCell.near_seed_frontier line 782

Source documentation

When a small ball meets the complement of the seed-ball domain, every inside point is close to its actual distance frontier.

lemma near_seed_frontier (x y z : M.Point J root) {ρ radius : ℝ}
    (hy : dist x y ≤ ρ) (hz : dist x z ≤ ρ)
    (hout : radius ≤ seedDistance S y) (hin : seedDistance S z ≤ radius) :
    ∃ w : M.Point J root, seedDistance S w=radius ∧ dist z w ≤ 2*ρ := by
…

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

lemma OAI.PlanarL1.Columns.Model.SecondaryCell.replacement_boundary_ball line 795
Source documentation
The .199R spatial margin defeats the total 4+5 scalar slopes. Consequently an entire ball touching outside is unchanged, without paying the much larger height-shield Lipschitz constant.
```
lemma replacement_boundary_ball (hS : S.Nonempty) (hOld : LipschitzWith 5 old)
    (hL : LipschitzWith 1 L) (hζ : R.ζ = (1:ℝ)/10)
    {pc radius αo : ℝ} (hr : 0 ≤ radius) (hαo : αo ≤ radius/1000)
    (hδ : R.δ = (radius/1000)/8) {α : Point.RadialTree.Noise (n := n)} (hα : R.NoiseBounds α)
…
```
Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.localAtomConstant_probability line 833

lemma OAI.PlanarL1.Columns.Model.SecondaryCell.namedReplacement_local_list line 890

Source documentation

All seed groups may use the same geometric radial hierarchy. The hierarchy and the whole local list are chosen before their independent samples.

lemma namedReplacement_local_list (hζ : R.ζ = (1:ℝ)/10)
    {k : ℕ} (A : R.Node k) (x : M.Point J root) {ρ : ℝ}
    (hlo : ∀ z : M.Point J root, dist x z ≤ ρ →
      (k:ℝ)*R.δ ≤ dist R.base (z.withHeight R.base.height R.base.inBand))
    (heq : ∀ (p : M.Point J root → ℝ) (α : Point.RadialTree.Noise (n := n)),
…

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

def OAI.PlanarL1.Columns.Model.SecondaryCell.simultaneousNamed line 924
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.sampledReplacement_lipschitz line 932
lemma OAI.PlanarL1.Columns.Model.SecondaryCell.simultaneousNamed_local_probability line 943

theorem OAI.PlanarL1.Columns.Model.SecondaryCell.simultaneousNamed_probability line 1004

Source documentation

The actual simultaneous secondary finite maximum has a local name bound independent of graph size once seed packing bounds the number of groups.

theorem simultaneousNamed_probability {groups : ℕ}
    (seeds : Fin groups → Finset (M.Point J root)) (old : M.Point J root → ℝ)
    (supports : Fin groups → M.Point J root → ℝ) (ordinary : Bool)
    (hOld : LipschitzWith 5 old) (hL : ∀ g, LipschitzWith 1 (supports g))
    (hζ : R.ζ = (1:ℝ)/10) (pc : Fin groups → ℝ) (radius lo B : ℝ) (hB : 0 < B)
    (x : M.Point J root) {ρ : ℝ} (hρ : 0 ≤ ρ) (hs : ρ ≤ R.radius)
    (m : ℕ) (hm : 0 < m) :
    FiniteRandom.prob (fun ω : Fin groups →
      Point.RadialTree.GridSample (n := n) R.depthCap m × (Fin (m+1) × Fin (m+1)) =>
…

Mentions: OAI.PlanarL1.FiniteRandom.prob, OAI.PlanarL1.Columns.Model.Point.RadialTree.GridSample