Minkowski

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

noncomputable def CKN.Foundation.Parabolic.Morrey.morreyENormCell (p q : ℝ) (f : ParabolicPoint → ENNReal) (z : ParabolicPoint) (r : ℝ) : ENNReal

The Morrey cell for an extended nonnegative-valued function.

Equations

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

noncomputable def CKN.Foundation.Parabolic.Morrey.morreyENorm (p q : ℝ) (f : ParabolicPoint → ENNReal) : ENNReal

The extended nonnegative-valued Morrey seminorm.

Equations

• CKN.Foundation.Parabolic.Morrey.morreyENorm p q f = ⨆ (z : CKN.Foundation.Parabolic.ParabolicPoint), ⨆ (r : { r : ℝ // 0 < r }), CKN.Foundation.Parabolic.Morrey.morreyENormCell p q f z ↑r

theorem CKN.Foundation.Parabolic.Morrey.morreyENorm_ofReal_abs (p q : ℝ) (f : ParabolicPoint → ℝ) : (morreyENorm p q fun (z : ParabolicPoint) => ENNReal.ofReal |f z|) = morreyNorm p q f

theorem CKN.Foundation.Parabolic.Morrey.morreyNorm_holder {p p₁ p₂ q q₁ q₂ : ℝ} (hp₁ : 1 ≤ p₁) (hp₂ : 1 ≤ p₂) (hrelp : 1 / p = 1 / p₁ + 1 / p₂) (hrelq : 1 / q = 1 / q₁ + 1 / q₂) {f g : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) (hg : AEMeasurable g MeasureTheory.volume) : (morreyNorm p q fun (z : ParabolicPoint) => f z * g z) ≤ morreyNorm p₁ q₁ f * morreyNorm p₂ q₂ g

theorem CKN.Foundation.Parabolic.Morrey.morreyNorm_lower_integrability {p' p q : ℝ} (hp' : 1 ≤ p') (hpp : p' ≤ p) (hpq : p ≤ q) {f : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) : morreyNorm p' q f ≤ MeasureTheory.volume (parabolicCylinder 0 0 1) ^ (1 / p' - 1 / p) * morreyNorm p q f

theorem CKN.Foundation.Parabolic.Morrey.morreyNorm_lower_morrey_exponent {p q q' : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) (hpq' : p ≤ q') (hq'q : q' ≤ q) {f : ParabolicPoint → ℝ} {z₀ : ParabolicPoint} {R : ℝ} (hR : 0 < R) (hsupp : ∀ w ∉ parabolicCylinder z₀.1 z₀.2 R, f w = 0) : morreyNorm p q' f ≤ ENNReal.ofReal R ^ (5 * (1 / q' - 1 / q)) * morreyNorm p q f

theorem CKN.Foundation.Parabolic.Morrey.morreyENorm_lintegral_le {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] {p q : ℝ} (hp : 1 ≤ p) : p ≤ q → ∀ {F : α × ParabolicPoint → ENNReal} (hF : AEMeasurable F (μ.prod MeasureTheory.volume)), (morreyENorm p q fun (z : ParabolicPoint) => ∫⁻ (w : α), F (w, z) ∂μ) ≤ ∫⁻ (w : α), morreyENorm p q fun (z : ParabolicPoint) => F (w, z) ∂μ

theorem CKN.Foundation.Parabolic.Morrey.morreyENorm_translate (p q : ℝ) (f : ParabolicPoint → ENNReal) (a : Vec3) (τ : ℝ) : (morreyENorm p q fun (w : ParabolicPoint) => f (parabolicTranslate a τ w)) = morreyENorm p q f

noncomputable def CKN.Foundation.Parabolic.Morrey.parabolicConvolution (K f : ParabolicPoint → ENNReal) (z : ParabolicPoint) : ENNReal

Extended nonnegative convolution with respect to parabolic translation.

Equations

• CKN.Foundation.Parabolic.Morrey.parabolicConvolution K f z = ∫⁻ (w : CKN.Foundation.Parabolic.ParabolicPoint), K w * f (CKN.Foundation.Parabolic.parabolicTranslate (-w.1) (-w.2) z)

theorem CKN.Foundation.Parabolic.Morrey.morreyENorm_parabolicConvolution_le {p q : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) {K f : ParabolicPoint → ENNReal} (hF : AEMeasurable (fun (wz : ParabolicPoint × ParabolicPoint) => K wz.1 * f (parabolicTranslate (-wz.1.1) (-wz.1.2) wz.2)) (MeasureTheory.volume.prod MeasureTheory.volume)) (hKtop : ∀ (w : ParabolicPoint), K w ≠ ⊤) (hfinit : morreyENorm p q f ≠ ⊤) : morreyENorm p q (parabolicConvolution K f) ≤ (∫⁻ (w : ParabolicPoint), K w) * morreyENorm p q f

noncomputable def CKN.Foundation.Parabolic.Morrey.spatialConvolution (K : Vec3 → ENNReal) (f : ParabolicPoint → ENNReal) (z : ParabolicPoint) : ENNReal

Spatial convolution of a parabolic source at each fixed time.

Equations

• CKN.Foundation.Parabolic.Morrey.spatialConvolution K f z = ∫⁻ (y : CKN.Foundation.Parabolic.Vec3), K y * f (CKN.Foundation.Parabolic.parabolicTranslate (-y) 0 z)

theorem CKN.Foundation.Parabolic.Morrey.morreyENorm_spatialConvolution_le {p q : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) {K : Vec3 → ENNReal} {f : ParabolicPoint → ENNReal} (hF : AEMeasurable (fun (yz : Vec3 × ParabolicPoint) => K yz.1 * f (parabolicTranslate (-yz.1) 0 yz.2)) (MeasureTheory.volume.prod MeasureTheory.volume)) (hKtop : ∀ (y : Vec3), K y ≠ ⊤) (hfinit : morreyENorm p q f ≠ ⊤) : morreyENorm p q (spatialConvolution K f) ≤ (∫⁻ (y : Vec3), K y) * morreyENorm p q f