Caccioppoli Energy Terms #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.caccioppoli_rhs_terms_bound
{Ω : 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)
(hscale : r ≤ ρ / 2)
(hεr : ε < r ^ 2)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
(hfuture : Set.Icc t₀ (t₀ + ε) ⊆ I)
{c : Foundation.Parabolic.ParabolicPoint → ℝ}
(hA :
AEMeasurable
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
ENNReal.ofReal |Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 2 - c w|)
(MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ)))
(hcm : AEMeasurable c (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ)))
(hcenter :
(∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal |Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 2 - c w| ^ (3 / 2)) ^ (2 / 3) ≤ ENNReal.ofReal (poincareSobolevL1VectorConstant * ρ ^ (4 / 3) * alpha u (x₀, t₀) ρ * beta u Du (x₀, t₀) ρ))
(hcc : ∀ (w : Foundation.Parabolic.ParabolicPoint), c w = c (x₀, w.2))
(hvelocity :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≠ ⊤)
(t : ℝ)
:
t ≤ t₀ →
∫ (s : ℝ) in Set.Iio t, ∫ (x : Foundation.Parabolic.Vec3) in Ω, localEnergyRhs u p f (backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r) (x, s) ≤ caccioppoliI1HeatCutoffRaw hρ hε + caccioppoliI2HeatCutoffRaw hρ hε + caccioppoliI3HeatCutoffRaw hρ hε + caccioppoliI4HeatCutoffRaw hρ hε