Far Oscillation #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_two_step_oscillation
{K : Foundation.Parabolic.ParabolicPoint → ℝ}
{z p p' v : Foundation.Parabolic.ParabolicPoint}
{r A B : ℝ}
(hp : p ∈ Metric.closedBall z r)
(hp' : p' ∈ Metric.closedBall z r)
(hA : 0 ≤ A)
(hB : 0 ≤ B)
(hspace :
|K (p.1 - v.1, p.2 - v.2) - K (p'.1 - v.1, p.2 - v.2)| ≤ A * Foundation.Parabolic.vec3EuclideanNorm (p.1 - p'.1))
(htime : |K (p'.1 - v.1, p.2 - v.2) - K (p'.1 - v.1, p'.2 - v.2)| ≤ B * |p.2 - p'.2|)
:
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_kernel_difference_abs_le_of_positive
{z p p' v : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
{j : ℕ}
(hr : 0 < r)
(hp : p ∈ Metric.closedBall z r)
(hp' : p' ∈ Metric.closedBall z r)
(hv : v ∈ heatPotentialFarShellSet z r j)
:
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_spatial_kernel_spatial_difference_abs_le_of_positive
{i : Fin 3}
{z p p' v : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
{j : ℕ}
(hr : 0 < r)
(hp : p ∈ Metric.closedBall z r)
(hp' : p' ∈ Metric.closedBall z r)
(hv : v ∈ heatPotentialFarShellSet z r j)
:
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_integral_oscillation_bound
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{z p p' : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
{j : ℕ}
{C : ℝ}
{M : ENNReal}
(hr : 0 < r)
(hF : AEMeasurable F MeasureTheory.volume)
(hp : p ∈ Metric.closedBall z r)
(hp' : p' ∈ Metric.closedBall z r)
(hfinite : ∫⁻ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, ENNReal.ofReal |F v| < ⊤)
(hMtop : M ≠ ⊤)
(hM : ∫⁻ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, ENNReal.ofReal |F v| ≤ M)
(hpoint : ∀ v ∈ heatPotentialFarShellSet z r j, |heatPotentialKernel p v - heatPotentialKernel p' v| ≤ C)
(hC : 0 ≤ C)
:
|(∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, heatPotentialKernel p v * F v) - ∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, heatPotentialKernel p' v * F v| ≤ C * M.toReal
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_spatial_integral_oscillation_bound
{i : Fin 3}
{G : Foundation.Parabolic.ParabolicPoint → ℝ}
{z p p' : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
{j : ℕ}
{C : ℝ}
{M : ENNReal}
(hr : 0 < r)
(hG : AEMeasurable G MeasureTheory.volume)
(hp : p ∈ Metric.closedBall z r)
(hp' : p' ∈ Metric.closedBall z r)
(hfinite : ∫⁻ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, ENNReal.ofReal |G v| < ⊤)
(hMtop : M ≠ ⊤)
(hM : ∫⁻ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, ENNReal.ofReal |G v| ≤ M)
(hpoint :
∀ v ∈ heatPotentialFarShellSet z r j, |heatPotentialSpatialKernel i p v - heatPotentialSpatialKernel i p' v| ≤ C)
(hC : 0 ≤ C)
:
|(∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, heatPotentialSpatialKernel i p v * G v) - ∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, heatPotentialSpatialKernel i p' v * G v| ≤ C * M.toReal
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_integral_oscillation_bound_of_morrey
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{z p p' : Foundation.Parabolic.ParabolicPoint}
{r P θ : ℝ}
{j : ℕ}
(hr : 0 < r)
(hP : 1 ≤ P)
(hPθ : P ≤ θ)
(hF : AEMeasurable F MeasureTheory.volume)
(hN : Foundation.Parabolic.Morrey.morreyNorm P θ F < ⊤)
(hp : p ∈ Metric.closedBall z r)
(hp' : p' ∈ Metric.closedBall z r)
:
|(∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, heatPotentialKernel p v * F v) - ∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, heatPotentialKernel p' v * F v| ≤ 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
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_spatial_integral_oscillation_bound_of_morrey
{i : Fin 3}
{G : Foundation.Parabolic.ParabolicPoint → ℝ}
{z p p' : Foundation.Parabolic.ParabolicPoint}
{r P θ : ℝ}
{j : ℕ}
(hr : 0 < r)
(hP : 1 ≤ P)
(hPθ : P ≤ θ)
(hG : AEMeasurable G MeasureTheory.volume)
(hN : Foundation.Parabolic.Morrey.morreyNorm P θ G < ⊤)
(hp : p ∈ Metric.closedBall z r)
(hp' : p' ∈ Metric.closedBall z r)
:
|(∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, heatPotentialSpatialKernel i p v * G v) - ∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, heatPotentialSpatialKernel i p' v * G v| ≤ 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).toReal
theorem
CKN.Core.HeatPotential.heatPotential_integral_near_far_split
{f : Foundation.Parabolic.ParabolicPoint → ℝ}
{z : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
(hcover : Set.univ = heatPotentialNearSet z r ∪ ⋃ (j : ℕ), heatPotentialFarShellSet z r j)
(hdST : ∀ (j : ℕ), Disjoint (heatPotentialNearSet z r) (heatPotentialFarShellSet z r j))
(hdT : Pairwise (Function.onFun Disjoint (heatPotentialFarShellSet z r)))
(hInt :
MeasureTheory.IntegrableOn f (heatPotentialNearSet z r ∪ ⋃ (j : ℕ), heatPotentialFarShellSet z r j)
MeasureTheory.volume)
:
∫ (v : Foundation.Parabolic.ParabolicPoint), f v = (∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialNearSet z r, f v) + ∑' (j : ℕ), ∫ (v : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, f v