Adams M4

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

noncomputable def CKN.Foundation.Parabolic.Morrey.parabolicAdamsMaximalConstant (P τ : ℝ) : ENNReal

A concrete constant for the localized maximal-function estimate.

Equations

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

noncomputable def CKN.Foundation.Parabolic.Morrey.parabolicAdamsPotentialConstant (β P τ : ℝ) : ENNReal

A concrete constant in the parabolic Adams inequality.

Equations

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

theorem CKN.Foundation.Parabolic.Morrey.morreyCell_toReal_le_lintegral_rpow {p q : ℝ} (hp : 0 ≤ p) {G : ParabolicPoint → ENNReal} {z : ParabolicPoint} {r : ℝ} : morreyCell p q (fun (w : ParabolicPoint) => (G w).toReal) z r ≤ ENNReal.ofReal r ^ (-(5 * (1 - p / q) / p)) * (∫⁻ (w : ParabolicPoint) in parabolicCylinder z.1 z.2 r, G w ^ p) ^ (1 / p)

The real-valued Morrey cell is controlled by the corresponding ENNReal integral.

theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszPotential_adams {P τ β : ℝ} (hP : 1 < P) (hPτ : P ≤ τ) (hβ : 0 < β) (hβτ : β * τ < 5) {f : ParabolicPoint → ℝ} (hf : Measurable f) : (morreyNorm (P / (1 - β * τ / 5)) (τ / (1 - β * τ / 5)) fun (z : ParabolicPoint) => (parabolicRieszPotential β f z).toReal) ≤ parabolicAdamsPotentialConstant β P τ * morreyNorm P τ f

Adams's Morrey estimate in the range 1 < P ≤ τ and 0 < βτ < 5.