Source Morrey Data

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

Product estimates used by the divergence-form sources. The cutoff factors are deliberately represented by their finite Morrey norms here; the smooth compact-support cutoff API supplies those bounds at the point where a cutoff is chosen.

theorem CKN.Core.Step4.source_product_morrey_bound {P P₁ P₂ θ θ₁ θ₂ : ℝ} (hP₁ : 1 ≤ P₁) (hP₂ : 1 ≤ P₂) (hrelP : 1 / P = 1 / P₁ + 1 / P₂) (hrelθ : 1 / θ = 1 / θ₁ + 1 / θ₂) {f g : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) (hg : AEMeasurable g MeasureTheory.volume) (h₁ : Foundation.Parabolic.Morrey.morreyNorm P₁ θ₁ f < ⊤) (h₂ : Foundation.Parabolic.Morrey.morreyNorm P₂ θ₂ g < ⊤) : (Foundation.Parabolic.Morrey.morreyNorm P θ fun (z : Foundation.Parabolic.ParabolicPoint) => f z * g z) < ⊤ ∧ (Foundation.Parabolic.Morrey.morreyNorm P θ fun (z : Foundation.Parabolic.ParabolicPoint) => f z * g z) ≤ Foundation.Parabolic.Morrey.morreyNorm P₁ θ₁ f * Foundation.Parabolic.Morrey.morreyNorm P₂ θ₂ g

theorem CKN.Core.Step4.source_heat_kernel_data_of_morrey {g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {P θ₀ θ₁ : ℝ} (hP : 1 ≤ P) (hPθ₀ : P ≤ θ₀) (hPθ₁ : P ≤ θ₁) (hP6 : P ≤ 6) (hδ₀ : 0 < 2 - 5 / θ₀) (hδ₁ : 0 < 1 - 5 / θ₁) (hg : ∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) MeasureTheory.volume) (hh : ∀ (j i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => h j z i) MeasureTheory.volume) (hNg : ∀ (i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm P θ₀ fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) < ⊤) (hNh : ∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm P θ₁ fun (z : Foundation.Parabolic.ParabolicPoint) => h j z i) < ⊤) (hsg : ∀ (i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) (hsh : ∀ (j i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => h j z i) : (∀ (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3), MeasureTheory.Integrable (fun (w : Foundation.Parabolic.ParabolicPoint) => HeatPotential.heatPotentialKernel z w * g w i) MeasureTheory.volume) ∧ ∀ (z : Foundation.Parabolic.ParabolicPoint) (j i : Fin 3), MeasureTheory.Integrable (fun (w : Foundation.Parabolic.ParabolicPoint) => HeatPotential.heatPotentialSpatialKernel j z w * h j w i) MeasureTheory.volume