Subordinated Far

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

theorem CKN.Core.HeatPotential.heatPotential_kernel_integrable_on_split {F : Foundation.Parabolic.ParabolicPoint → ℝ} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ} {z p : Foundation.Parabolic.ParabolicPoint} {r P θ₀ θ₁ : ℝ} (hr : 0 < r) (hP : 1 ≤ P) (hPθ₀ : P ≤ θ₀) (hPθ₁ : P ≤ θ₁) (hF : AEMeasurable F MeasureTheory.volume) (hG : ∀ (i : Fin 3), AEMeasurable (G i) MeasureTheory.volume) (hNF : Foundation.Parabolic.Morrey.morreyNorm P θ₀ F < ⊤) (hNG : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm P θ₁ (G i) < ⊤) (hSupportF : HasCompactSupport F) (hSupportG : ∀ (i : Fin 3), HasCompactSupport (G i)) (hδ₀ : 0 < 2 - 5 / θ₀) (hδ₁ : 0 < 1 - 5 / θ₁) (hp : p ∈ Metric.closedBall z r) : MeasureTheory.IntegrableOn (fun (v : Foundation.Parabolic.ParabolicPoint) => heatPotentialKernel p v * F v) (heatPotentialNearSet z r ∪ ⋃ (j : ℕ), heatPotentialFarShellSet z r j) MeasureTheory.volume ∧ ∀ (i : Fin 3), MeasureTheory.IntegrableOn (fun (v : Foundation.Parabolic.ParabolicPoint) => heatPotentialSpatialKernel i p v * G i v) (heatPotentialNearSet z r ∪ ⋃ (j : ℕ), heatPotentialFarShellSet z r j) MeasureTheory.volume

theorem CKN.Core.HeatPotential.heatPotential_near_oscillation_bound_of_morrey {F : Foundation.Parabolic.ParabolicPoint → ℝ} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ} {z p p' : Foundation.Parabolic.ParabolicPoint} {r γ θ₀ θ₁ P : ℝ} (hr : 0 < r) (hγ : 0 < γ) (hθ₀ : 1 / θ₀ = (2 - γ) / 5) (hθ₁ : 1 / θ₁ = (1 - γ) / 5) (hP : 1 ≤ P) (hPθ₀ : P ≤ θ₀) (hPθ₁ : P ≤ θ₁) (hF : AEMeasurable F MeasureTheory.volume) (hG : ∀ (i : Fin 3), AEMeasurable (G i) MeasureTheory.volume) (hNF : Foundation.Parabolic.Morrey.morreyNorm P θ₀ F < ⊤) (hNG : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm P θ₁ (G i) < ⊤) (hp : p ∈ Metric.closedBall z r) (hp' : p' ∈ Metric.closedBall z r) : |((∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialNearSet z r, heatPotentialKernel p v * F v) + ∑ i : Fin 3, ∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialNearSet z r, heatPotentialSpatialKernel i p v * G i v) - ((∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialNearSet z r, heatPotentialKernel p' v * F v) + ∑ i : Fin 3, ∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialNearSet z r, heatPotentialSpatialKernel i p' v * G i v)| ≤ (2 * 1000 * 2 ^ (8 - 5 / θ₀) * (1 - 2 ^ (-γ))⁻¹ * 256 ^ γ * (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1)).toReal ^ (1 - 1 / P) * (Foundation.Parabolic.Morrey.morreyNorm P θ₀ F).toReal + ∑ i : Fin 3, 2 * 300000 * 2 ^ (10 - 1 - 5 / θ₁) * (1 - 2 ^ (-γ))⁻¹ * 256 ^ γ * (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1)).toReal ^ (1 - 1 / P) * (Foundation.Parabolic.Morrey.morreyNorm P θ₁ (G i)).toReal) * r ^ γ

theorem CKN.Core.HeatPotential.heatPotential_far_shell_oscillation_bound_of_morrey {F : Foundation.Parabolic.ParabolicPoint → ℝ} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ} {z p p' : Foundation.Parabolic.ParabolicPoint} {r P θ₀ θ₁ : ℝ} {j : ℕ} (hr : 0 < r) (hP : 1 ≤ P) (hPθ₀ : P ≤ θ₀) (hPθ₁ : P ≤ θ₁) (hF : AEMeasurable F MeasureTheory.volume) (hG : ∀ (i : Fin 3), AEMeasurable (G i) MeasureTheory.volume) (hNF : Foundation.Parabolic.Morrey.morreyNorm P θ₀ F < ⊤) (hNG : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm P θ₁ (G i) < ⊤) (hp : p ∈ Metric.closedBall z r) (hp' : p' ∈ Metric.closedBall z r) : |heatPotentialShellValue F G (heatPotentialFarShellSet z r j) p - heatPotentialShellValue F G (heatPotentialFarShellSet z r j) p'| ≤ 2 * r * (900000 / (2 ^ (↑j + 4) * r) ^ 4 + 2 * r * (10000000 / (2 ^ (↑j + 4) * r) ^ 5)) * (ENNReal.ofReal (2 * (2 ^ (↑(↑j + 6) + 1) * r)) ^ (5 * (1 - 1 / θ₀)) * MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (1 - 1 / P) * Foundation.Parabolic.Morrey.morreyNorm P θ₀ F).toReal + ∑ i : Fin 3, 2 * r * (60000000 / (2 ^ (↑j + 4) * r) ^ 5 + 2 * r * (30000000000 / (2 ^ (↑j + 4) * r) ^ 6)) * (ENNReal.ofReal (2 * (2 ^ (↑(↑j + 6) + 1) * r)) ^ (5 * (1 - 1 / θ₁)) * MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (1 - 1 / P) * Foundation.Parabolic.Morrey.morreyNorm P θ₁ (G i)).toReal