Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Parabolic.Morrey.Adams

Hedberg and Adams estimates #

This module connects the parabolic Riesz potential with the exported maximal function estimates and the cylinder Morrey seminorm.

source
noncomputable def CKN.Foundation.Parabolic.Morrey.parabolicMaximalMajorant (f : ParabolicPoint → ℝ) :
ParabolicPoint → ENNReal

The maximal function applied to the absolute value of a real function.

Equations
Instances For
    source
    theorem CKN.Foundation.Parabolic.Morrey.isParabolicMaximalMajorant_parabolicMaximalMajorant (f : ParabolicPoint → ℝ) :
    IsParabolicMaximalMajorant f (parabolicMaximalMajorant f)

    The maximal majorant property of the exported parabolic maximal function.

    source
    def CKN.Foundation.Parabolic.Morrey.nearShell (R : ℝ) (n : ℕ) (z : ParabolicPoint) :
    Set ParabolicPoint

    Negative-index dyadic parabolic shell for the near-field Morrey estimate.

    Equations
    Instances For
      source
      noncomputable def CKN.Foundation.Parabolic.Morrey.parabolicHedbergNearConstant (β : ℝ) :
      ENNReal

      The geometric constant in the local Hedberg estimate.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszPotential_near_le {β q : ℝ} (hβ : 0 < β) (hβ5 : β < 5) (hq : 1 ≤ q) (hβq : β * q < 5) {R : ℝ} (hR : 0 < R) {f : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) {M : ParabolicPoint → ENNReal} (hM : IsParabolicMaximalMajorant f M) (z : ParabolicPoint) :
        ∫⁻ (w : ParabolicPoint) in {w : ParabolicPoint | parabolicRho₂ z w < R}, parabolicRieszKernel β z w * ENNReal.ofReal |f w| ≤ parabolicHedbergNearConstant β * ENNReal.ofReal (R ^ β) * M z

        The local part of the potential is bounded by the maximal majorant.

        source
        theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszPotential_scale_le {β q : ℝ} (hβ : 0 < β) (hβ5 : β < 5) (hq : 1 ≤ q) (hβq : β * q < 5) {R : ℝ} (hR : 0 < R) {f : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) {M : ParabolicPoint → ENNReal} (hM : IsParabolicMaximalMajorant f M) (z : ParabolicPoint) :
        parabolicRieszPotential β f z ≤ parabolicHedbergNearConstant β * ENNReal.ofReal (R ^ β) * M z + parabolicTailKernelConstant β q * ENNReal.ofReal R ^ (β - 5 / q) * morreyNorm 1 q f

        The two-scale Hedberg estimate before optimization.

        source
        theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszPotential_hedberg_of_balance {β q : ℝ} (hβ : 0 < β) (hβ5 : β < 5) (hq : 1 ≤ q) (hβq : β * q < 5) {R : ℝ} (hR : 0 < R) {f : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) {M : ParabolicPoint → ENNReal} (hM : IsParabolicMaximalMajorant f M) {N : ENNReal} (hN : N = morreyNorm 1 q f) (z : ParabolicPoint) (hM0 : M z ≠ 0) (hMtop : M z ≠ ⊤) :
        N ≠ 0 → N ≠ ⊤ → ∀ (hbalance : ENNReal.ofReal R ^ (5 / q) * M z = N), parabolicRieszPotential β f z ≤ (parabolicHedbergNearConstant β + parabolicTailKernelConstant β q) * M z ^ (1 - β * q / 5) * N ^ (β * q / 5)

        Hedberg's pointwise estimate at a scale satisfying the balancing identity.

        source
        theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszPotential_hedberg {β q : ℝ} (hβ : 0 < β) (hβ5 : β < 5) (hq : 1 ≤ q) (hβq : β * q < 5) {f : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) {M : ParabolicPoint → ENNReal} (hM : IsParabolicMaximalMajorant f M) (z : ParabolicPoint) (hM0 : M z ≠ 0) (hMtop : M z ≠ ⊤) (hN : morreyNorm 1 q f ≠ 0) (hNtop : morreyNorm 1 q f ≠ ⊤) :
        parabolicRieszPotential β f z ≤ (parabolicHedbergNearConstant β + parabolicTailKernelConstant β q) * M z ^ (1 - β * q / 5) * morreyNorm 1 q f ^ (β * q / 5)

        Hedberg's pointwise estimate for positive finite maximal and Morrey data.