Morrey Sources

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

theorem CKN.Core.HeatPotential.heatPotential_shell_source_l1_bound {F : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} {r P θ : ℝ} (hr : 0 < r) (hP : 1 ≤ P) (hPθ : P ≤ θ) (hF : AEMeasurable F MeasureTheory.volume) (k : ℤ) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.Morrey.parabolicRieszShell r k z, ENNReal.ofReal |F w| ≤ ENNReal.ofReal (2 * (2 ^ (↑k + 1) * r)) ^ (5 * (1 - 1 / θ)) * MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (1 - 1 / P) * Foundation.Parabolic.Morrey.morreyNorm P θ F

theorem CKN.Core.HeatPotential.heatPotential_near_riesz_shell_term_bound {F : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} {r P θ β : ℝ} (hr : 0 < r) (hP : 1 ≤ P) (hPθ : P ≤ θ) (hβ5 : β < 5) (hF : AEMeasurable F MeasureTheory.volume) (n : ℕ) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.Morrey.parabolicRieszShell r (Int.negSucc n) z, Foundation.Parabolic.Morrey.parabolicRieszKernel β z w * ENNReal.ofReal |F w| ≤ ENNReal.ofReal (2 ^ ↑(Int.negSucc n) * r) ^ (-(5 - β)) * ENNReal.ofReal (2 * (2 ^ (↑(Int.negSucc n) + 1) * r)) ^ (5 * (1 - 1 / θ)) * MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (1 - 1 / P) * Foundation.Parabolic.Morrey.morreyNorm P θ F

theorem CKN.Core.HeatPotential.integrableOn_abs_of_lintegral_lt_top {F : Foundation.Parabolic.ParabolicPoint → ℝ} {S : Set Foundation.Parabolic.ParabolicPoint} (hF : AEMeasurable F MeasureTheory.volume) (hfinite : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in S, ENNReal.ofReal |F w| < ⊤) : MeasureTheory.IntegrableOn (fun (w : Foundation.Parabolic.ParabolicPoint) => |F w|) S MeasureTheory.volume

theorem CKN.Core.HeatPotential.integrableOn_of_abs_integrable {F : Foundation.Parabolic.ParabolicPoint → ℝ} {S : Set Foundation.Parabolic.ParabolicPoint} (hF : AEMeasurable F MeasureTheory.volume) (hfinite : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in S, ENNReal.ofReal |F w| < ⊤) : MeasureTheory.IntegrableOn F S MeasureTheory.volume

theorem CKN.Core.HeatPotential.integrableOn_mul_of_abs_integrable_of_bound {F K : Foundation.Parabolic.ParabolicPoint → ℝ} {S : Set Foundation.Parabolic.ParabolicPoint} {C : ℝ} (hS : MeasurableSet S) (hF : AEMeasurable F MeasureTheory.volume) (hK : AEMeasurable K MeasureTheory.volume) (hfinite : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in S, ENNReal.ofReal |F w| < ⊤) : 0 ≤ C → ∀ (hbound : ∀ w ∈ S, |K w| ≤ C), MeasureTheory.IntegrableOn (fun (w : Foundation.Parabolic.ParabolicPoint) => K w * F w) S MeasureTheory.volume

theorem CKN.Core.HeatPotential.real_integral_abs_le_of_lintegral_le {F : Foundation.Parabolic.ParabolicPoint → ℝ} {S : Set Foundation.Parabolic.ParabolicPoint} {M : ENNReal} (hF : AEMeasurable F MeasureTheory.volume) (hfinite : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in S, ENNReal.ofReal |F w| < ⊤) (hMtop : M ≠ ⊤) (hM : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in S, ENNReal.ofReal |F w| ≤ M) : ∫ (w : Foundation.Parabolic.ParabolicPoint) in S, |F w| ≤ M.toReal

theorem CKN.Core.HeatPotential.heatPotential_near_shell_geometric_sum {A : ℕ → ENNReal} {C q : ENNReal} : q < 1 → ∀ (hA : ∀ (n : ℕ), A n ≤ C * q ^ n), ∑' (n : ℕ), A n ≤ C * (1 - q)⁻¹