Maximal-majorant interface for the Hedberg estimate

The maximal theorem is deliberately not reproved here. This module gives the parameter property used by the pointwise potential argument and records the exponent identities needed by its eventual proof.

def CKN.Foundation.Parabolic.Morrey.IsParabolicMaximalMajorant (f : ParabolicPoint → ℝ) (M : ParabolicPoint → ENNReal) : Prop

A function is a parabolic uncentred maximal majorant for f.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Foundation.Parabolic.Morrey.hedbergMorreyExponent (β q : ℝ) : ℝ

The Morrey exponent in the Hedberg inequality.

Equations

• CKN.Foundation.Parabolic.Morrey.hedbergMorreyExponent β q = β * q / 5

theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszPotential_split {β : ℝ} {f : ParabolicPoint → ℝ} (z : ParabolicPoint) {R : ℝ} : parabolicRieszPotential β f z = (∫⁻ (w : ParabolicPoint) in {w : ParabolicPoint | parabolicRho₂ z w < R}, parabolicRieszKernel β z w * ENNReal.ofReal |f w|) + ∫⁻ (w : ParabolicPoint) in {w : ParabolicPoint | R ≤ parabolicRho₂ z w}, parabolicRieszKernel β z w * ENNReal.ofReal |f w|

theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszPotential_split_le {β : ℝ} {f : ParabolicPoint → ℝ} (z : ParabolicPoint) {R : ℝ} {A B : ENNReal} (hnear : ∫⁻ (w : ParabolicPoint) in {w : ParabolicPoint | parabolicRho₂ z w < R}, parabolicRieszKernel β z w * ENNReal.ofReal |f w| ≤ A) (hfar : ∫⁻ (w : ParabolicPoint) in {w : ParabolicPoint | R ≤ parabolicRho₂ z w}, parabolicRieszKernel β z w * ENNReal.ofReal |f w| ≤ B) : parabolicRieszPotential β f z ≤ A + B