Envelopes.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GeometricFilter.filt line 57
Source documentation
Causal dyadic averaging, with both the present and the complete past.
```
def filt (c : ℕ → ℝ) : ℕ → ℝ
  | 0 => c 0
  | i+1 => c (i+1)+filt c i/2
```
lemma OAI.GeometricFilter.filt_nonneg line 60
lemma OAI.GeometricFilter.le_filt line 64
lemma OAI.GeometricFilter.filt_le line 68
lemma OAI.GeometricFilter.filt_mono line 72
lemma OAI.GeometricFilter.filt_mul line 76
lemma OAI.GeometricFilter.filt_sum line 80
lemma OAI.GeometricFilter.filt_tail_strong line 97

theorem OAI.GeometricFilter.filt_tail line 115

Source documentation

The complete pre-birth history costs a fixed amount, not the birth index.

theorem filt_tail {c : ℕ → ℝ} {A : ℝ} (hA : 0 ≤ A) (hc0 : ∀ i, 0 ≤ c i)
    (hcA : ∀ i, c i ≤ A) {b m : ℕ} (hbm : b ≤ m) :
    (∑ i ∈ Ico b (m+1), filt c i) ≤ 2*∑ i ∈ Ico b (m+1), c i+4*A := by
…

Mentions: OAI.GeometricFilter.filt

theorem OAI.GeometricFilter.double_tail line 123

Source documentation

Two geometric convolutions are summable on every occupied lifetime.

theorem double_tail {c : ℕ → ℝ} {A : ℝ} (hA : 0 ≤ A) (hc0 : ∀ i, 0 ≤ c i)
    (hcA : ∀ i, c i ≤ A) {b m : ℕ} (hbm : b ≤ m) :
    (∑ i ∈ Ico b (m+1), filt (filt c) i) ≤ 4*∑ i ∈ Ico b (m+1), c i+16*A := by
…

Mentions: OAI.GeometricFilter.filt

lemma OAI.GeometricFilter.radius_sum line 133
def OAI.ActualLabels.spatialConstant line 151
lemma OAI.ActualLabels.spatialConstant_pos line 152
lemma OAI.ActualLabels.spatialConstant_ge line 156
lemma OAI.ActualLabels.scaled_marginal_distance line 160

theorem OAI.ActualLabels.filtered_spatial_cost line 175

Source documentation

Actual spatial comparison at every point of the neighborhood. The gradient versions are pointwise bounded; differentiability is only needed later for IBP.

theorem filtered_spatial_cost (h : ℂ → ℂ) (r : ℕ → ℝ) (q : ℕ → ℤ × ℤ)
    (x y : ℂ) (j : ℕ) (hr : ∀ i ≤ j, 0 < r i)
    (hstep : ∀ i < j, r i = 2*r (i+1))
    (hx : ∀ i ≤ j, boxNorm (x-point (r i) (q i)) < 199*r i)
    (hy : ∀ i ≤ j, boxNorm (y-point (r i) (q i)) < 199*r i)
    (hdist : ‖x-y‖ ≤ 104*r j) :
    switchCost h r x j+derivativeCost h r x j ≤
      spatialConstant*filt (energyRate h r q y) j := by
…

Mentions: OAI.ActualLabels.switchCost, OAI.ActualLabels.derivativeCost, OAI.ActualLabels.spatialConstant, OAI.ActualLabels.energyRate

lemma OAI.DyadicHats.scale_mono line 229
lemma OAI.DyadicHats.descending_step line 231
lemma OAI.DyadicHats.descending_compare line 234
def OAI.DyadicHats.neighborhood line 239
lemma OAI.DyadicHats.point_mem_neighborhood line 240
def OAI.ActualMarkTrees.pathVertex line 249
lemma OAI.ActualMarkTrees.terminal_path_locality line 251

lemma OAI.ActualMarkTrees.path_neighborhood_geometry line 264

Source documentation

The neighborhoods used by assembly remain within the actual 200-neighbor energy window at every earlier row, including the complete pre-birth history.

lemma path_neighborhood_geometry {N : ℕ} (v : Grid N → ℂ) {r : ℝ} (hr : 0 < r)
    {m : ℕ} {q : Grid N} {p : List (Grid N)} (hp : activePath (tree v m 1 q) p)
    {l : ℕ} (hl : l ≤ m) {x : ℂ}
    (hx : x ∈ neighborhood (scale r (m-l)) (pathVertex q p l))
    {i : ℕ} (hi : i ≤ m) (hil : i ≤ l+1) :
    ‖x-point r (lastVertex q p)‖ ≤ 104*scale r (m-i) ∧
    boxNorm (x-point (scale r (m-i)) (pathVertex q p i)) < 199*scale r (m-i) ∧
    boxNorm (point r (lastVertex q p)-point (scale r (m-i)) (pathVertex q p i)) < 199*scale r (m-i) := by
…

Mentions: OAI.ActualMarkTrees.tree, OAI.ActualMarkTrees.pathVertex, OAI.ActualMarkTrees.lastVertex

lemma OAI.GeometricFilter.filt_mono_on line 291
lemma OAI.GeometricFilter.shifted_tail line 295
def OAI.DyadicHats.localSup line 305
lemma OAI.DyadicHats.localSup_le line 307
lemma OAI.DyadicHats.le_localSup line 312
lemma OAI.DyadicHats.localSup_nonneg line 315
lemma OAI.ActualLabels.derivativeCost_nonneg line 322
def OAI.ActualLabels.cellCost line 328
lemma OAI.ActualLabels.cellCost_nonneg line 333
lemma OAI.ActualMarkTrees.path_filtered_cost line 347
lemma OAI.ActualMarkTrees.path_cellCost line 361
lemma OAI.ActualMarkTrees.path_cellCost_sum line 399
def OAI.ActualMarkTrees.packingCharge line 425
lemma OAI.ActualMarkTrees.packingCharge_path line 428
lemma OAI.ActualMarkTrees.tree_packing_bound line 458
def OAI.ActualMarkTrees.packingConstant line 470
lemma OAI.ActualMarkTrees.packingConstant_pos line 473
theorem OAI.ActualMarkTrees.spatial_packing line 478
def OAI.CommonPrices.rootMass line 514
lemma OAI.CommonPrices.rootMass_nonneg line 516
def OAI.CommonPrices.sizeErrors line 519
lemma OAI.CommonPrices.sizeErrors_price line 525
lemma OAI.CommonPrices.sizeErrors_gradient line 544

theorem OAI.CommonPrices.size_cell_price line 561

Source documentation

The endpoint-bin gradient price, with all root terms retained rather than silently using the cone estimate at one-sided maximizing radii.

theorem size_cell_price : ∃ C : ℝ, 0 < C ∧
    ∀ {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R) (hN : R/r+1 ≤ (N:ℝ))
    {g : ℂ → ℝ}, ContDiff ℝ 1 g → Integrable (gradient g) →
    (∀ y, gradient g y ≠ 0 → ‖y‖ ≤ R) → ∀ (k : ℕ) (p : ℤ × ℤ)
    {n : ℂ}, n ∈ fixedPalette.labels → ∀ Q : Set ℂ, volume Q ≤ ENNReal.ofReal 1 →
    ∃ F : ℂ → ℝ≥0∞, Measurable F ∧
      (∫⁻ X in Q, F X) ≤ ENNReal.ofReal (C*(scale r k)⁻¹*
        (rootMass (gradient g) r k (cellRoots N p)+cellPrice N r (gradient g) k (cellRoots N p))) ∧
      ∀ X, ‖X‖ ≤ 2 → ∀ t,
        EndpointRadius (fun Y => g (point (scale r k) p+scale r k • Y)) X t →
        ENNReal.ofReal ‖∫ Y in Metric.ball X t,
          gradient (fun Z => g (point (scale r k) p+scale r k • Z)) Y‖ ≤ F X := by
…

Mentions: OAI.CommonPrices.rootMass, OAI.CommonPrices.cellRoots, OAI.CommonPrices.cellPrice