Ambient.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.PlanarL1.Columns.Model.Ambient line 15
Source documentation
Full columns regarded in the unrestricted path pseudometric. Connectedness here is supplied by the connected graph realization, not an extra condition on the embedding theorem.
```
structure Ambient (M : Model (k+1)) where
…
```
Mentions: OAI.PlanarL1.Columns.Model
def OAI.PlanarL1.Columns.Model.Ambient.point line 22
lemma OAI.PlanarL1.Columns.Model.Ambient.point_dist line 25
lemma OAI.PlanarL1.Columns.Model.Ambient.point_switch line 28
lemma OAI.PlanarL1.Columns.Model.Ambient.taper_switch line 34

def OAI.PlanarL1.Columns.Model.Ambient.historyField line 43

Source documentation

Every signed increment from the recorded lifetime is retained. Regions are those at their creation times and are not re-tapered after subsequent changes.

noncomputable def historyField {I : Set ℝ} (s : M.Field I 4) (a b : Fin (k+1))
    {m : ℕ} (r : Fin m → ℝ) (regions : Fin m → Set (M.Point Set.univ A.root))
    (sign : Fin m → Bool) (c : ℝ) (hc : 0 < c) (hcr : c ≤ 4)
    (hr : ∀ j, 0 < r j)
    (hsep : ∀ i j, i ≠ j → 10*r i ≤ c*r j ∨ 10*r j ≤ c*r i) : M.Field I 100 where
…

structure OAI.PlanarL1.Columns.Model.Ambient.History line 84
Source documentation
The literal finite list of increments already recorded for an identifier. Regions are recorded at creation time, as required by .
```
structure History (A : Ambient M) (c : ℝ) where
…
```
Mentions: OAI.PlanarL1.Columns.Model.Ambient
def OAI.PlanarL1.Columns.Model.Ambient.History.empty line 95
def OAI.PlanarL1.Columns.Model.Ambient.History.field line 103
lemma OAI.PlanarL1.Columns.Model.Ambient.History.field_empty line 107
def OAI.PlanarL1.Columns.Model.Ambient.History.append line 113

lemma OAI.PlanarL1.Columns.Model.Ambient.History.field_append_value line 136

Source documentation

No earlier summand is re-tapered or otherwise modified by appending a step.

lemma field_append_value (H : History A c) (r : ℝ) (S : Set (M.Point Set.univ A.root))
    (e : Bool) (hr : 0 < r) (hcross : ∀ j, 10*r ≤ c*H.radius j)
    {I : Set ℝ} (s : M.Field I 4) (a b : Fin (k+1)) (hc : 0 < c) (hcr : c ≤ 4)
    (i : Fin (k+1)) (T : I) :
    ((H.append r S e hr hcross).field s a b hc hcr).value i T =
      (H.field s a b hc hcr).value i T+
      Increment.signedDamped e (c*r) r ((s.transverse (by norm_num) a b).value i)
        (fun U : I => Increment.taper Sᶜ r (A.point i U.val)) T := by
…

Mentions: OAI.PlanarL1.Columns.Model.Ambient.History, OAI.PlanarL1.Columns.Model.Ambient.History.field, OAI.PlanarL1.Increment.signedDamped, OAI.PlanarL1.Increment.taper

def OAI.PlanarL1.Columns.Model.BData.Recorded line 166
def OAI.PlanarL1.Columns.Model.BData.incrementAuxiliary line 171

lemma OAI.PlanarL1.Columns.Model.BData.increment_difference line 180

Source documentation

The actual recorded increment, not a replacement of the old history.

lemma increment_difference (D : OrderedData M) (H : A.History c)
    (r : ℝ) (region : Set (M.Point Set.univ A.root)) (e : Bool)
    (hc : 0 < c) (hcr : c ≤ 4) (hr : 0 < r)
    (hcross : ∀ j, 10*r ≤ c*H.radius j)
    (hrec : (BData.ordered D).Recorded H hc hcr)
    (lam : ℝ≥0) (hlam : lam ≤ (1:ℝ≥0)/100)
    (i : Fin (k+1)) (T : D.band) :
    ((BData.ordered D).auxiliaryField
      ((BData.ordered D).incrementAuxiliary H r region e hc hcr hr hcross) lam hlam).value i T -
      D.value lam i T =
      lam*Increment.signedDamped e (c*r) r ((D.base.transverse (by norm_num) D.lower D.upper).value i)
        (fun U : D.band => Increment.taper regionᶜ r (A.point i U.val)) T := by
…

Mentions: OAI.PlanarL1.Columns.Model.OrderedData, OAI.PlanarL1.Columns.Model.BData.Recorded, OAI.PlanarL1.Columns.Model.BData.auxiliaryField, OAI.PlanarL1.Columns.Model.BData.incrementAuxiliary, OAI.PlanarL1.Columns.Model.BData.value, OAI.PlanarL1.Increment.signedDamped, OAI.PlanarL1.Increment.taper

lemma OAI.PlanarL1.Columns.Model.BData.increment_boundary line 197
def OAI.PlanarL1.Columns.Model.BData.incrementHistory line 223
Source documentation
Ordinary identifiers record no increments. Ordered identifiers keep the entire old list and append precisely the new signed region-tapered term.
```
def incrementHistory (D : BData M) (H : A.History c)
    (r : ℝ) (region : Set (M.Point Set.univ A.root)) (e : Bool)
    (hr : 0 < r) (hcross : ∀ j, 10*r ≤ c*H.radius j) : A.History c :=
…
```
Mentions: OAI.PlanarL1.Columns.Model.BData
lemma OAI.PlanarL1.Columns.Model.BData.increment_recorded line 230
lemma OAI.PlanarL1.Columns.Model.BData.increment_magnitude line 240
def OAI.PlanarL1.Columns.Model.BState.region line 280
Source documentation
A region is exactly the old identifier's inverse image in the full-column ambient model. No approximation of its boundary is used.
```
def region (a : Fin (S.count+1)) : Set (M.Point Set.univ A.root) :=
…
```
lemma OAI.PlanarL1.Columns.Model.BState.other_height_not_region line 283
def OAI.PlanarL1.Columns.Model.BState.incrementFields line 287
lemma OAI.PlanarL1.Columns.Model.BState.increment_boundary line 295
def OAI.PlanarL1.Columns.Model.BState.increment line 314
lemma OAI.PlanarL1.Columns.Model.BState.increment_names line 325
lemma OAI.PlanarL1.Columns.Model.BState.increment_recorded line 334
lemma OAI.PlanarL1.Columns.Model.BState.increment_movement line 345