OAI/Analysis/LipschitzHilbert/Trees/SourceKernelIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual positive kernel tail is controlled by interval averages. The constant is independent of the spatial scale.

  1. theorem OAI.LipschitzHilbert.kernel_integral_of_interval_bounds line 12
  2. theorem OAI.LipschitzHilbert.kernel_integral_le_threeGridMaximal line 76

    Source documentation

    The kernel centered at any point within one scale of the evaluation point is bounded by its actual three-grid maximal majorant.

    theorem kernel_integral_le_threeGridMaximal (f : ℝ → ℝ) (hf : Measurable f)
    (hLp : MemLp f 2 volume) (C : ℝ) (hf0 : ∀ x, 0≤f x) (hbound : ∀ x, ‖f x‖≤C) :
    ∀ᵐ z ∂volume, ∀ c r : ℝ, 0<r → |z-c|≤r →
      (∫ x, r⁻¹*lineEnvelope c r 1 x*f x)≤96*DyadicLineGrid.threeGridMaximal f z := by
…

    Mentions: OAI.LipschitzHilbert.lineEnvelope, OAI.LipschitzHilbert.DyadicLineGrid.threeGridMaximal