Subordinated Assembly #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_profile_of_morrey
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ}
{r γ θ₀ θ₁ P : ℝ}
(hr : 0 < r)
:
0 < γ →
∀ (hθ₀ : 1 / θ₀ = (2 - γ) / 5) (hθ₁ : 1 / θ₁ = (1 - γ) / 5),
1 ≤ P →
P ≤ θ₀ →
P ≤ θ₁ →
Foundation.Parabolic.Morrey.morreyNorm P θ₀ F < ⊤ →
(∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm P θ₁ (G i) < ⊤) →
have V := (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1)).toReal;
have BF := V ^ (1 - 1 / P) * (Foundation.Parabolic.Morrey.morreyNorm P θ₀ F).toReal;
have BG := fun (i : Fin 3) =>
V ^ (1 - 1 / P) * (Foundation.Parabolic.Morrey.morreyNorm P θ₁ (G i)).toReal;
have A := fun (j : ℕ) =>
2 * r * (900000 / (2 ^ (↑j + 4) * r) ^ 4 + 2 * r * (10000000 / (2 ^ (↑j + 4) * r) ^ 5)) * ((2 * (2 ^ (↑(↑j + 6) + 1) * r)) ^ (5 * (1 - 1 / θ₀)) * BF) + ∑ i : Fin 3,
2 * r * (60000000 / (2 ^ (↑j + 4) * r) ^ 5 + 2 * r * (30000000000 / (2 ^ (↑j + 4) * r) ^ 6)) * ((2 * (2 ^ (↑(↑j + 6) + 1) * r)) ^ (5 * (1 - 1 / θ₁)) * BG i);
have C :=
(1800000 * 2 ^ (8 * (5 * (1 - 1 / θ₀)) - 16) + 40000000 * 2 ^ (8 * (5 * (1 - 1 / θ₀)) - 20)) * BF + ∑ i : Fin 3,
(120000000 * 2 ^ (8 * (5 * (1 - 1 / θ₁)) - 20) + 120000000000 * 2 ^ (8 * (5 * (1 - 1 / θ₁)) - 24)) * BG i;
(∀ (j : ℕ), 0 ≤ A j) ∧ ∀ (j : ℕ), A j ≤ C * 2 ^ (↑j * (γ - 1)) * r ^ γ
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_value_bound_of_morrey
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ}
{z p p' : Foundation.Parabolic.ParabolicPoint}
{r γ θ₀ θ₁ P : ℝ}
(hr : 0 < r)
:
0 < γ →
1 / θ₀ = (2 - γ) / 5 →
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),
have V := (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1)).toReal;
have BF := V ^ (1 - 1 / P) * (Foundation.Parabolic.Morrey.morreyNorm P θ₀ F).toReal;
have BG := fun (i : Fin 3) => V ^ (1 - 1 / P) * (Foundation.Parabolic.Morrey.morreyNorm P θ₁ (G i)).toReal;
have A := fun (j : ℕ) =>
2 * r * (900000 / (2 ^ (↑j + 4) * r) ^ 4 + 2 * r * (10000000 / (2 ^ (↑j + 4) * r) ^ 5)) * ((2 * (2 ^ (↑(↑j + 6) + 1) * r)) ^ (5 * (1 - 1 / θ₀)) * BF) + ∑ i : Fin 3,
2 * r * (60000000 / (2 ^ (↑j + 4) * r) ^ 5 + 2 * r * (30000000000 / (2 ^ (↑j + 4) * r) ^ 6)) * ((2 * (2 ^ (↑(↑j + 6) + 1) * r)) ^ (5 * (1 - 1 / θ₁)) * BG i);
∀ (j : ℕ),
|heatPotentialShellValue F G (heatPotentialFarShellSet z r j) p - heatPotentialShellValue F G (heatPotentialFarShellSet z r j) p'| ≤ A j
theorem
CKN.Core.HeatPotential.heatPotential_series_difference_bound
{h : Foundation.Parabolic.ParabolicPoint → ℝ}
{s : ℕ → Foundation.Parabolic.ParabolicPoint → ℝ}
{p p' : Foundation.Parabolic.ParabolicPoint}
{Anear : ℝ}
{A : ℕ → ℝ}
{n : Foundation.Parabolic.ParabolicPoint → ℝ}
(hsplitp : h p = n p + ∑' (j : ℕ), s j p)
(hsplitp' : h p' = n p' + ∑' (j : ℕ), s j p')
(hsump : Summable fun (j : ℕ) => s j p)
(hsump' : Summable fun (j : ℕ) => s j p')
(hnear : |n p - n p'| ≤ Anear)
(hAsum : Summable A)
(hfar : ∀ (j : ℕ), |s j p - s j p'| ≤ A j)
: