OAI/Analysis/LipschitzHilbert/Trees/SourceKernelShells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Dyadic annuli for a reproducing-kernel bound by actual interval averages. Closed outer intervals and open inner intervals retain every boundary point.

  1. def OAI.LipschitzHilbert.kernelShell line 14
  2. theorem OAI.LipschitzHilbert.kernelShell_measurable line 19
  3. theorem OAI.LipschitzHilbert.kernelShell_subset line 24
  4. theorem OAI.LipschitzHilbert.kernelShell_covers line 30
  5. theorem OAI.LipschitzHilbert.kernelShell_lower line 47
  6. theorem OAI.LipschitzHilbert.kernelShell_envelope line 60

    Source documentation

    The inverse quadratic envelope has a geometric shell bound; after multiplication by shell length, the remaining series has ratio one half.

    theorem kernelShell_envelope (c r : ℝ) (hr : 0<r) (n : ℕ) {x : ℝ}
    (hx : x∈kernelShell c r n) :
    lineEnvelope c r 1 x≤4/((2:ℝ)^n)^2 := by
…

    Mentions: OAI.LipschitzHilbert.kernelShell, OAI.LipschitzHilbert.lineEnvelope