OAI/Analysis/LipschitzHilbert/Trees/GeometricBoundaryDepth.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.geometricBoundaryLayer line 16
2. def OAI.LipschitzHilbert.geometricBoundaryDepth line 19
3. theorem OAI.LipschitzHilbert.geometricBoundaryLayer_nonneg line 22
4. theorem OAI.LipschitzHilbert.geometricBoundaryLayer_integrable line 26
5. theorem OAI.LipschitzHilbert.integral_geometricBoundaryLayer line 31
6. theorem OAI.LipschitzHilbert.integral_norm_geometricBoundaryLayer line 37
7. theorem OAI.LipschitzHilbert.integral_geometricBoundaryDepth line 44

   Source documentation

   The boundary-depth average is finite and has the exact geometric-series value. This avoids any loss depending on the number of angular levels.

   theorem integral_geometricBoundaryDepth {ε q : ℝ}
       (hε : 0 ≤ ε) (hq : 0 ≤ q) (hq1 : q < 1) :
       (∫ b, geometricBoundaryDepth ε q b) = ε / (1 - q) := by
   …

   Mentions: OAI.LipschitzHilbert.geometricBoundaryDepth

8. theorem OAI.LipschitzHilbert.geometricBoundaryDepth_integrable line 56
9. theorem OAI.LipschitzHilbert.integral_geometricBoundaryDepth_le line 65

   Source documentation

   With angular branching at least two, the average depth costs at most 2ε, independent of the depth of the hierarchy.

   theorem integral_geometricBoundaryDepth_le {ε G : ℝ} (hε : 0 ≤ ε) (hG : 2 ≤ G) :
       (∫ b, geometricBoundaryDepth ε G⁻¹ b) ≤ 2 * ε := by
   …

   Mentions: OAI.LipschitzHilbert.geometricBoundaryDepth