Subordinated Base

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

theorem CKN.Core.HeatPotential.positive_shell_exists {z w : Foundation.Parabolic.ParabolicPoint} {R : ℝ} (hR : 0 < R) (hRρ : R ≤ Foundation.Parabolic.Morrey.parabolicRho₂ z w) : ∃ (k : ℕ), w ∈ Foundation.Parabolic.Morrey.parabolicRieszShell R (↑k) z

theorem CKN.Core.HeatPotential.shell_scale_sixtyfour {z w : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (n : ℕ) : w ∈ Foundation.Parabolic.Morrey.parabolicRieszShell (64 * r) (↑n) z ↔ w ∈ Foundation.Parabolic.Morrey.parabolicRieszShell r (↑n + 6) z

theorem CKN.Core.HeatPotential.heatPotential_near_far_cover {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) : Set.univ = heatPotentialNearSet z r ∪ ⋃ (j : ℕ), heatPotentialFarShellSet z r j

theorem CKN.Core.HeatPotential.heatPotential_near_far_disjoint {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (j : ℕ) : Disjoint (heatPotentialNearSet z r) (heatPotentialFarShellSet z r j)

theorem CKN.Core.HeatPotential.heatPotential_far_shells_pairwise_disjoint {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) : Pairwise (Function.onFun Disjoint (heatPotentialFarShellSet z r))

theorem CKN.Core.HeatPotential.heatPotential_source_integrable_of_compact_support {F : Foundation.Parabolic.ParabolicPoint → ℝ} {P θ : ℝ} (hP : 1 ≤ P) (hPθ : P ≤ θ) (hF : AEMeasurable F MeasureTheory.volume) (hN : Foundation.Parabolic.Morrey.morreyNorm P θ F < ⊤) (hSupport : HasCompactSupport F) : MeasureTheory.Integrable F MeasureTheory.volume

theorem CKN.Core.HeatPotential.rhoTwo_eq_parabolicRho₂ {z w : Foundation.Parabolic.ParabolicPoint} {ht : 0 < z.2 - w.2} : Foundation.Heat.rhoTwo (z.1 - w.1) (z.2 - w.2) = Foundation.Parabolic.Morrey.parabolicRho₂ z w

theorem CKN.Core.HeatPotential.parabolicRho₂_pos_of_time {z w : Foundation.Parabolic.ParabolicPoint} {ht : 0 < z.2 - w.2} : 0 < Foundation.Parabolic.Morrey.parabolicRho₂ z w

theorem CKN.Core.HeatPotential.heatPotentialKernel_abs_le_riesz₂ (z w : Foundation.Parabolic.ParabolicPoint) : |heatPotentialKernel z w| ≤ 1000 * (Foundation.Parabolic.Morrey.parabolicRieszKernel 2 z w).toReal

theorem CKN.Core.HeatPotential.heatPotentialSpatialKernel_abs_le_riesz₁ (i : Fin 3) (z w : Foundation.Parabolic.ParabolicPoint) : |heatPotentialSpatialKernel i z w| ≤ 300000 * (Foundation.Parabolic.Morrey.parabolicRieszKernel 1 z w).toReal

theorem CKN.Core.HeatPotential.heatPotential_rho_zero_null (z : Foundation.Parabolic.ParabolicPoint) : MeasureTheory.volume {w : Foundation.Parabolic.ParabolicPoint | Foundation.Parabolic.Morrey.parabolicRho₂ z w = 0} = 0

theorem CKN.Core.HeatPotential.heatPotential_near_riesz_le_shells {F : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} {R β : ℝ} (hR : 0 < R) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in {w : Foundation.Parabolic.ParabolicPoint | Foundation.Parabolic.Morrey.parabolicRho₂ z w < R}, Foundation.Parabolic.Morrey.parabolicRieszKernel β z w * ENNReal.ofReal |F w| ≤ ∑' (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|

theorem CKN.Core.HeatPotential.heatPotential_near_riesz_scale {β θ R : ℝ} {n : ℕ} (hR : 0 < R) : ENNReal.ofReal (2 ^ ↑(Int.negSucc n) * R) ^ (-(5 - β)) * ENNReal.ofReal (2 * (2 ^ (↑(Int.negSucc n) + 1) * R)) ^ (5 * (1 - 1 / θ)) = ENNReal.ofReal 2 ^ (10 - β - 5 / θ) * (ENNReal.ofReal 2 ^ (-(β - 5 / θ))) ^ n * ENNReal.ofReal R ^ (β - 5 / θ)

theorem CKN.Core.HeatPotential.heatPotential_near_riesz_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) : Foundation.Parabolic.Morrey.morreyNorm P θ F < ⊤ → ∀ (hδ : 0 < β - 5 / θ), ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in {w : Foundation.Parabolic.ParabolicPoint | Foundation.Parabolic.Morrey.parabolicRho₂ z w < R}, Foundation.Parabolic.Morrey.parabolicRieszKernel β z w * ENNReal.ofReal |F w| ≤ ENNReal.ofReal 2 ^ (10 - β - 5 / θ) * (1 - ENNReal.ofReal 2 ^ (-(β - 5 / θ)))⁻¹ * ENNReal.ofReal R ^ (β - 5 / θ) * MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (1 - 1 / P) * Foundation.Parabolic.Morrey.morreyNorm P θ F

theorem CKN.Core.HeatPotential.heatPotential_riesz_ne_top_of_pos {β : ℝ} {z w : Foundation.Parabolic.ParabolicPoint} (hρ : 0 < Foundation.Parabolic.Morrey.parabolicRho₂ z w) : Foundation.Parabolic.Morrey.parabolicRieszKernel β z w ≠ ⊤

theorem CKN.Core.HeatPotential.heatPotential_near_kernel_abs_lintegral_bound {F : Foundation.Parabolic.ParabolicPoint → ℝ} {p : Foundation.Parabolic.ParabolicPoint} {R P θ : ℝ} (hR : 0 < R) (hP : 1 ≤ P) (hPθ : P ≤ θ) (hF : AEMeasurable F MeasureTheory.volume) (hN : Foundation.Parabolic.Morrey.morreyNorm P θ F < ⊤) (hδ : 0 < 2 - 5 / θ) : ∫⁻ (v : Foundation.Parabolic.ParabolicPoint) in {v : Foundation.Parabolic.ParabolicPoint | Foundation.Parabolic.Morrey.parabolicRho₂ p v < R}, ENNReal.ofReal |heatPotentialKernel p v * F v| ≤ 1000 * (ENNReal.ofReal 2 ^ (8 - 5 / θ) * (1 - ENNReal.ofReal 2 ^ (-(2 - 5 / θ)))⁻¹ * ENNReal.ofReal R ^ (2 - 5 / θ) * MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (1 - 1 / P) * Foundation.Parabolic.Morrey.morreyNorm P θ F)

theorem CKN.Core.HeatPotential.heatPotential_near_spatial_kernel_abs_lintegral_bound {i : Fin 3} {G : Foundation.Parabolic.ParabolicPoint → ℝ} {p : Foundation.Parabolic.ParabolicPoint} {R P θ : ℝ} (hR : 0 < R) (hP : 1 ≤ P) (hPθ : P ≤ θ) (hG : AEMeasurable G MeasureTheory.volume) (hN : Foundation.Parabolic.Morrey.morreyNorm P θ G < ⊤) (hδ : 0 < 1 - 5 / θ) : ∫⁻ (v : Foundation.Parabolic.ParabolicPoint) in {v : Foundation.Parabolic.ParabolicPoint | Foundation.Parabolic.Morrey.parabolicRho₂ p v < R}, ENNReal.ofReal |heatPotentialSpatialKernel i p v * G v| ≤ 300000 * (ENNReal.ofReal 2 ^ (10 - 1 - 5 / θ) * (1 - ENNReal.ofReal 2 ^ (-(1 - 5 / θ)))⁻¹ * ENNReal.ofReal R ^ (1 - 5 / θ) * MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (1 - 1 / P) * Foundation.Parabolic.Morrey.morreyNorm P θ G)

theorem CKN.Core.HeatPotential.heatPotential_far_shell_source_factor_toReal {F : Foundation.Parabolic.ParabolicPoint → ℝ} {r P θ : ℝ} (hr : 0 < r) : AEMeasurable F MeasureTheory.volume → Foundation.Parabolic.Morrey.morreyNorm P θ F < ⊤ → ∀ (j : ℕ), (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 = (2 * (2 ^ (↑(↑j + 6) + 1) * r)) ^ (5 * (1 - 1 / θ)) * (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1)).toReal ^ (1 - 1 / P) * (Foundation.Parabolic.Morrey.morreyNorm P θ F).toReal

theorem CKN.Core.HeatPotential.heatPotential_far_scale_first {a r c : ℝ} {m j : ℕ} (hr : 0 < r) : 2 * r * (c / (2 ^ (↑j + 4) * r) ^ m) * (2 * (2 ^ (↑j + 7) * r)) ^ a = 2 * c * 2 ^ (8 * a - 4 * ↑m) * 2 ^ (↑j * (a - ↑m)) * r ^ (a + 1 - ↑m)

theorem CKN.Core.HeatPotential.heatPotential_far_scale_second {a r c : ℝ} {m j : ℕ} (hr : 0 < r) : 2 * r * (2 * r * (c / (2 ^ (↑j + 4) * r) ^ m)) * (2 * (2 ^ (↑j + 7) * r)) ^ a = 4 * c * 2 ^ (8 * a - 4 * ↑m) * 2 ^ (↑j * (a - ↑m)) * r ^ (a + 2 - ↑m)