Caccioppoli Mean Subtraction #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.caccioppoli_poincare_radius
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{z₀ : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hΩ : IsOpen Ω)
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 ρ) ⊆ spaceTimeSet Ω I)
:
∃ (R : ℝ), ρ < R ∧ Foundation.Parabolic.vec3Ball z₀.1 R ⊆ Ω
theorem
CKN.caccioppoli_local_energy_ae
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hψ : ψ ∈ spaceTimeTestFunction Ω I)
(hψ_nonneg : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ ψ z)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, (∫ (x : Foundation.Parabolic.Vec3) in Ω, Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ^ 2 * ψ (x, t)) + 2 * ∫ (s : ℝ) in Set.Iio t, ∫ (x : Foundation.Parabolic.Vec3) in Ω, spatialGradientSq u Du (x, s) * ψ (x, s) ≤ ∫ (s : ℝ) in Set.Iio t, ∫ (x : Foundation.Parabolic.Vec3) in Ω, localEnergyRhs u p f ψ (x, s)
theorem
CKN.caccioppoli_localEnergyRhs_decompose
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ}
(z : Foundation.Parabolic.ParabolicPoint)
:
localEnergyRhs u p f ψ z = Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * ∑ i : Fin 3, u z i * spatialPartial ψ i z + 2 * p z * ∑ i : Fin 3, u z i * spatialPartial ψ i z + (2 * ∑ i : Fin 3, f z i * u z i) * ψ z
theorem
CKN.caccioppoli_local_energy_ae_decomposed
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hψ : ψ ∈ spaceTimeTestFunction Ω I)
(hψ_nonneg : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ ψ z)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, (∫ (x : Foundation.Parabolic.Vec3) in Ω, Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ^ 2 * ψ (x, t)) + 2 * ∫ (s : ℝ) in Set.Iio t, ∫ (x : Foundation.Parabolic.Vec3) in Ω, spatialGradientSq u Du (x, s) * ψ (x, s) ≤ ∫ (s : ℝ) in Set.Iio t, ∫ (x : Foundation.Parabolic.Vec3) in Ω, Foundation.Parabolic.vec3EuclideanNorm (u (x, s)) ^ 2 * (timePartial ψ (x, s) + ∑ i : Fin 3, spatialSecondPartial ψ i i (x, s)) + Foundation.Parabolic.vec3EuclideanNorm (u (x, s)) ^ 2 * ∑ i : Fin 3, u (x, s) i * spatialPartial ψ i (x, s) + 2 * p (x, s) * ∑ i : Fin 3, u (x, s) i * spatialPartial ψ i (x, s) + (2 * ∑ i : Fin 3, f (x, s) i * u (x, s) i) * ψ (x, s)
theorem
CKN.caccioppoli_slice_poincare_ae
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
:
∃ (R : ℝ) (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ),
ρ < R ∧ localBox Ω I Ω' J ∧ (∀ x ∈ Foundation.Parabolic.vec3Ball x₀ R, x ∈ Ω') ∧ (∀ s ∈ Set.Ioc (t₀ - ρ ^ 2) t₀, s ∈ J) ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀), (∫ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, |Foundation.Parabolic.vec3EuclideanNorm (u (x, s)) ^ 2 - ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 2| ^ (3 / 2)) ^ (2 / 3) ≤ poincareSobolevL1VectorConstant * (∫ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (u (x, s)) ^ 2) ^ (1 / 2) * (∫ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, spatialGradientSq u Du (x, s)) ^ (1 / 2)
theorem
CKN.caccioppoli_heat_cutoff_cancel
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ ε r : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
(hr : 0 < r)
(hεr : ε < r ^ 2)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
(hfuture : Set.Icc t₀ (t₀ + ε) ⊆ I)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀), ∀ (x : ℝ),
parametricPairing
(fun (s : ℝ) (y : Foundation.Parabolic.Vec3) =>
backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r (y, s))
(fun (x : Foundation.Parabolic.Vec3) => 0) (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(fun (x : Foundation.Parabolic.Vec3) => 0) x = 0