OAI/Analysis/SignedDisk/ActualLabels1.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedDisk.ActualLabels.energyRate line 33
2. lemma OAI.SignedDisk.ActualLabels.energyRate_nonneg line 35
3. lemma OAI.SignedDisk.ActualLabels.energyRate_le_five line 37
4. theorem OAI.SignedDisk.ActualLabels.marginal_spatial_distance line 46

   Source documentation

   Spatial comparison of the actual marginal laws. No independent coupling or pointwise uniform distribution of labels is assumed.

   theorem marginal_spatial_distance (h : ℂ → ℂ) (r : ℕ → ℝ) (q : ℕ → ℤ × ℤ)
       (x y : ℂ) (j : ℕ) (hr : ∀ i ≤ j, 0 < r i)
       (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) :
       l1dist (marginal h r j x) (marginal h r j y) ≤
         comparisonConstant*‖x-y‖*∑ i ∈ range (j+1), energyRate h r q y i/r i := by
   …

   Mentions: OAI.SignedDisk.ActualLabels.marginal, OAI.SignedDisk.ActualLabels.comparisonConstant, OAI.SignedDisk.ActualLabels.energyRate

5. lemma OAI.SignedDisk.ActualLabels.switchCost_spatial line 84
6. lemma OAI.SignedDisk.ActualLabels.derivativeCost_spatial line 98
7. def OAI.SignedDisk.GeometricFilter.filt line 121

   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

8. lemma OAI.SignedDisk.GeometricFilter.filt_nonneg line 124
9. lemma OAI.SignedDisk.GeometricFilter.le_filt line 128
10. lemma OAI.SignedDisk.GeometricFilter.filt_le line 132
11. lemma OAI.SignedDisk.GeometricFilter.filt_mono line 136
12. lemma OAI.SignedDisk.GeometricFilter.filt_mul line 140
13. lemma OAI.SignedDisk.GeometricFilter.filt_sum line 144
14. lemma OAI.SignedDisk.GeometricFilter.filt_tail_strong line 161
15. theorem OAI.SignedDisk.GeometricFilter.filt_tail line 179

    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.SignedDisk.GeometricFilter.filt

16. theorem OAI.SignedDisk.GeometricFilter.double_tail line 187

    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.SignedDisk.GeometricFilter.filt

17. lemma OAI.SignedDisk.GeometricFilter.radius_sum line 195
18. def OAI.SignedDisk.ActualLabels.spatialConstant line 213
19. lemma OAI.SignedDisk.ActualLabels.spatialConstant_pos line 214
20. lemma OAI.SignedDisk.ActualLabels.spatialConstant_ge line 218
21. lemma OAI.SignedDisk.ActualLabels.scaled_marginal_distance line 222
22. theorem OAI.SignedDisk.ActualLabels.filtered_spatial_cost line 237

    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.SignedDisk.ActualLabels.switchCost, OAI.SignedDisk.ActualLabels.derivativeCost, OAI.SignedDisk.ActualLabels.spatialConstant, OAI.SignedDisk.ActualLabels.energyRate

23. lemma OAI.SignedDisk.DyadicHats.scale_mono line 291
24. lemma OAI.SignedDisk.DyadicHats.descending_step line 293
25. lemma OAI.SignedDisk.DyadicHats.descending_compare line 296
26. def OAI.SignedDisk.DyadicHats.neighborhood line 301
27. lemma OAI.SignedDisk.DyadicHats.point_mem_neighborhood line 302
28. def OAI.SignedDisk.ActualMarkTrees.pathVertex line 311
29. lemma OAI.SignedDisk.ActualMarkTrees.terminal_path_locality line 313
30. lemma OAI.SignedDisk.ActualMarkTrees.path_neighborhood_geometry line 326

    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.SignedDisk.ActualMarkTrees.tree, OAI.SignedDisk.ActualMarkTrees.pathVertex, OAI.SignedDisk.ActualMarkTrees.lastVertex

31. lemma OAI.SignedDisk.GeometricFilter.filt_mono_on line 353
32. lemma OAI.SignedDisk.GeometricFilter.shifted_tail line 357
33. def OAI.SignedDisk.DyadicHats.localSup line 367
34. lemma OAI.SignedDisk.DyadicHats.localSup_le line 369
35. lemma OAI.SignedDisk.DyadicHats.le_localSup line 374
36. lemma OAI.SignedDisk.DyadicHats.localSup_nonneg line 377
37. lemma OAI.SignedDisk.ActualLabels.derivativeCost_nonneg line 384
38. def OAI.SignedDisk.ActualLabels.cellCost line 390
39. lemma OAI.SignedDisk.ActualLabels.cellCost_nonneg line 395