OAI/Analysis/LipschitzHilbert/Trees/SourcePlanarKernelBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Product reproducing-kernel majorants are controlled by the actual strong maximal construction on the plane.

  1. def OAI.LipschitzHilbert.normalizedLineEnvelope line 13
  2. theorem OAI.LipschitzHilbert.normalizedLineEnvelope_measurable line 15
  3. theorem OAI.LipschitzHilbert.normalizedLineEnvelope_nonneg line 18
  4. theorem OAI.LipschitzHilbert.normalizedLineEnvelope_integrable line 22
  5. def OAI.LipschitzHilbert.verticalKernelAverage line 26
  6. theorem OAI.LipschitzHilbert.verticalKernelAverage_measurable line 29
  7. theorem OAI.LipschitzHilbert.verticalKernelAverage_le_maximal line 33
  8. theorem OAI.LipschitzHilbert.planar_kernel_le_strongMaximal line 60

    Source documentation

    The product kernel is bounded on its central rectangle by one strong maximal function, with constants independent of both scales.

    theorem planar_kernel_le_strongMaximal {U : ℝ×ℝ → ℝ}
    (hUm : Measurable U) (hU2 : MemLp U 2 (volume.prod volume))
    (B : ℝ) (hB : 0≤B) (hU0 : ∀ z, 0≤U z) (hUb : ∀ z, ‖U z‖≤B)
    (cx cy rx ry : ℝ) (hrx : 0<rx) (hry : 0<ry) :
    ∀ᵐ z ∂volume.prod volume, |z.1-cx|≤rx ∧ |z.2-cy|≤ry →
      (∫ p, normalizedLineEnvelope cx rx p.1*normalizedLineEnvelope cy ry p.2*U p
        ∂volume.prod volume)≤9216*threeStrongMaximal U z := by
…

    Mentions: OAI.LipschitzHilbert.normalizedLineEnvelope