BoundaryDepthCrossing.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The geometric envelope equals the first angular scale crossing, and hence controls the shifted differences of the actual boundary argument.

theorem OAI.LipschitzHilbert.geometricBoundaryDepth_eq_crossing line 15
theorem OAI.LipschitzHilbert.exists_geometricBoundaryDepth_crossing line 37
Source documentation
Every positive boundary distance has a finite first crossing scale. The geometric depth counts exactly the preceding scales.
```
theorem exists_geometricBoundaryDepth_crossing {ε q b : ℝ}
    (hε : 0 ≤ ε) (hq : 0 ≤ q) (hq1 : q < 1) (hb : 0 < b) :
    ∃ r : ℕ, geometricBoundaryDepth ε q b = (r : ℝ) ∧ ε * q ^ r ≤ b ∧
      ∀ j < r, b < ε * q ^ j := by
…
```
Mentions: OAI.LipschitzHilbert.geometricBoundaryDepth

theorem OAI.LipschitzHilbert.boundary_loss_le_geometricDepth line 57

Source documentation

The finite-difference estimate can use the first scale crossing directly, without losing the number of levels in the path.

theorem boundary_loss_le_geometricDepth (a loss : ℕ → ℝ) (k : ℕ) {ε q b B : ℝ}
    (hε : 0 ≤ ε) (hq : 0 ≤ q) (hq1 : q < 1) (hb : 0 < b)
    (ha : ∀ i, 0 ≤ a i) (hbound : ∀ i, a i ≤ B)
    (hloss : ∀ r : ℕ, ε * q ^ r ≤ b →
      ∀ i < k, loss i ≤ a i - a (i + r)) :
    (∑ i ∈ Finset.range k, loss i) ≤ geometricBoundaryDepth ε q b * B := by
…

Mentions: OAI.LipschitzHilbert.geometricBoundaryDepth