Subordinated Campanato #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Core.HeatPotential.heatPotential_campanato_bound_of_morrey
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ}
{z : Foundation.Parabolic.ParabolicPoint}
{r γ θ₀ θ₁ P : ℝ}
(hr : 0 < r)
(hγ : 0 < γ)
(hγ1 : γ < 1)
(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) < ⊤)
(hSupportF : HasCompactSupport F)
(hSupportG : ∀ (i : Fin 3), HasCompactSupport (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 Cnear :=
2 * 1000 * 2 ^ (8 - 5 / θ₀) * (1 - 2 ^ (-γ))⁻¹ * 256 ^ γ * BF + ∑ i : Fin 3, 2 * 300000 * 2 ^ (10 - 1 - 5 / θ₁) * (1 - 2 ^ (-γ))⁻¹ * 256 ^ γ * 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;
Foundation.Parabolic.ParabolicBallLpOscillation (heatPotential F G) z r P ≤ (Cnear + C * (1 - 2 ^ (γ - 1))⁻¹) * r ^ γ
theorem
CKN.Core.HeatPotential.heatPotential_global_campanato_bound_of_morrey
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ}
{γ θ₀ θ₁ P : ℝ}
(hγ : 0 < γ)
(hγ1 : γ < 1)
(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) < ⊤)
(hSupportF : HasCompactSupport F)
(hSupportG : ∀ (i : Fin 3), HasCompactSupport (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 Cnear :=
2 * 1000 * 2 ^ (8 - 5 / θ₀) * (1 - 2 ^ (-γ))⁻¹ * 256 ^ γ * BF + ∑ i : Fin 3, 2 * 300000 * 2 ^ (10 - 1 - 5 / θ₁) * (1 - 2 ^ (-γ))⁻¹ * 256 ^ γ * 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;
Foundation.Parabolic.GlobalParabolicBallCampanatoBound (heatPotential F G) γ (Cnear + C * (1 - 2 ^ (γ - 1))⁻¹) P
theorem
CKN.Core.HeatPotential.prop_heat_morrey_hoelder
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ}
{γ θ₀ θ₁ P : ℝ}
(hγ : 0 < γ)
(hγ1 : γ < 1)
(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) < ⊤)
(hSupportF : HasCompactSupport F)
(hSupportG : ∀ (i : Fin 3), HasCompactSupport (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 Cnear :=
2 * 1000 * 2 ^ (8 - 5 / θ₀) * (1 - 2 ^ (-γ))⁻¹ * 256 ^ γ * BF + ∑ i : Fin 3, 2 * 300000 * 2 ^ (10 - 1 - 5 / θ₁) * (1 - 2 ^ (-γ))⁻¹ * 256 ^ γ * 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;
∃ (barh : Foundation.Parabolic.ParabolicPoint → ℝ),
barh =ᵐ[MeasureTheory.volume] heatPotential F G ∧ Foundation.Parabolic.ParabolicHolderSeminormLE Set.univ barh γ
(Foundation.Parabolic.parabolicCampanatoHolderConstant γ P * (Cnear + C * (1 - 2 ^ (γ - 1))⁻¹)) ∧ ∀ (z : Foundation.Parabolic.ParabolicPoint) (R : ℝ),
0 < R →
∀ w ∈ Metric.ball z R,
|barh w| ≤ 2 ^ γ * (Foundation.Parabolic.parabolicCampanatoHolderConstant γ P * (Cnear + C * (1 - 2 ^ (γ - 1))⁻¹)) * R ^ γ + (⨍ (x : Foundation.Parabolic.ParabolicPoint) in Metric.ball z R, |heatPotential F G x| ^ P) ^ (1 / P)