Subordinated Near

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

theorem CKN.Core.HeatPotential.heatPotential_near_factor_toReal {δ q r b : ℝ} {N : ENNReal} (hr : 0 < r) (hδ : 0 < δ) : (ENNReal.ofReal 2 ^ q * (1 - ENNReal.ofReal 2 ^ (-δ))⁻¹ * ENNReal.ofReal (256 * r) ^ δ * MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ b * N).toReal = 2 ^ q * (1 - 2 ^ (-δ))⁻¹ * (256 * r) ^ δ * (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1)).toReal ^ b * N.toReal

theorem CKN.Core.HeatPotential.heatPotential_near_factor_ne_top {δ q r b : ℝ} {N : ENNReal} : 0 < r → ∀ (hδ : 0 < δ) (hq : 0 ≤ q) (hb : 0 ≤ b) (hN : N < ⊤), ENNReal.ofReal 2 ^ q * (1 - ENNReal.ofReal 2 ^ (-δ))⁻¹ * ENNReal.ofReal (256 * r) ^ δ * MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ b * N ≠ ⊤

theorem CKN.Core.HeatPotential.subordinated_parabolicRho₂_le_two_parabolicDist (z w : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.Morrey.parabolicRho₂ z w ≤ 2 * Foundation.Parabolic.parabolicDist z w

theorem CKN.Core.HeatPotential.subordinated_parabolicRho₂_quasi_triangle (a b c : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.Morrey.parabolicRho₂ a c ≤ 2 * Foundation.Parabolic.Morrey.parabolicRho₂ a b + 2 * Foundation.Parabolic.Morrey.parabolicRho₂ b c

theorem CKN.Core.HeatPotential.heatPotential_near_set_subset_riesz_ball {z p : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hp : p ∈ Metric.closedBall z r) : heatPotentialNearSet z r ⊆ {v : Foundation.Parabolic.ParabolicPoint | Foundation.Parabolic.Morrey.parabolicRho₂ p v < 256 * r}

theorem CKN.Core.HeatPotential.heatPotential_far_uniform_kernel_bound {z p : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hp : p ∈ Metric.closedBall z r) (v : Foundation.Parabolic.ParabolicPoint) : v ∈ ⋃ (j : ℕ), heatPotentialFarShellSet z r j → |heatPotentialKernel p v| ≤ 1000 / (16 * r) ^ 3

theorem CKN.Core.HeatPotential.heatPotential_far_uniform_spatial_kernel_bound {z p : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hp : p ∈ Metric.closedBall z r) (i : Fin 3) (v : Foundation.Parabolic.ParabolicPoint) : v ∈ ⋃ (j : ℕ), heatPotentialFarShellSet z r j → |heatPotentialSpatialKernel i p v| ≤ 300000 / (16 * r) ^ 4

theorem CKN.Core.HeatPotential.heatPotential_near_kernel_integrable {F : Foundation.Parabolic.ParabolicPoint → ℝ} {z 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 / θ) (hp : p ∈ Metric.closedBall z r) : MeasureTheory.IntegrableOn (fun (v : Foundation.Parabolic.ParabolicPoint) => heatPotentialKernel p v * F v) (heatPotentialNearSet z r) MeasureTheory.volume

theorem CKN.Core.HeatPotential.heatPotential_near_spatial_kernel_integrable {G : Foundation.Parabolic.ParabolicPoint → ℝ} {z 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 / θ) (hp : p ∈ Metric.closedBall z r) (i : Fin 3) : MeasureTheory.IntegrableOn (fun (v : Foundation.Parabolic.ParabolicPoint) => heatPotentialSpatialKernel i p v * G v) (heatPotentialNearSet z r) MeasureTheory.volume

theorem CKN.Core.HeatPotential.heatPotential_near_kernel_abs_integral_bound {F : Foundation.Parabolic.ParabolicPoint → ℝ} {z 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 / θ) (hp : p ∈ Metric.closedBall z r) : ∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialNearSet z r, |heatPotentialKernel p v * F v| ≤ 1000 * (2 ^ (8 - 5 / θ) * (1 - 2 ^ (-(2 - 5 / θ)))⁻¹ * 256 ^ (2 - 5 / θ) * (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1)).toReal ^ (1 - 1 / P) * (Foundation.Parabolic.Morrey.morreyNorm P θ F).toReal) * r ^ (2 - 5 / θ)

theorem CKN.Core.HeatPotential.heatPotential_near_spatial_kernel_abs_integral_bound {i : Fin 3} {G : Foundation.Parabolic.ParabolicPoint → ℝ} {z 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 / θ) (hp : p ∈ Metric.closedBall z r) : ∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialNearSet z r, |heatPotentialSpatialKernel i p v * G v| ≤ 300000 * (2 ^ (10 - 1 - 5 / θ) * (1 - 2 ^ (-(1 - 5 / θ)))⁻¹ * 256 ^ (1 - 5 / θ) * (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1)).toReal ^ (1 - 1 / P) * (Foundation.Parabolic.Morrey.morreyNorm P θ G).toReal) * r ^ (1 - 5 / θ)