Caccioppoli RHS #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.caccioppoli_dot_abs_le
(a b : Foundation.Parabolic.Vec3)
:
|∑ i : Fin 3, a i * b i| ≤ Foundation.Parabolic.vec3EuclideanNorm a * Foundation.Parabolic.vec3EuclideanNorm b
theorem
CKN.caccioppoli_partial_sum_abs
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{z : Foundation.Parabolic.ParabolicPoint}
:
|∑ i : Fin 3, u z i * spatialPartial F i z| ≤ Foundation.Parabolic.vec3EuclideanNorm (u z) * ∑ i : Fin 3, |spatialPartial F i z|
theorem
CKN.caccioppoli_force_abs_le
{u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{z : Foundation.Parabolic.ParabolicPoint}
(hF : 0 ≤ F z)
:
theorem
CKN.caccioppoli_heat_cutoff_tsupport_subset
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ ε r : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
:
ContDiff ℝ (↑⊤) (backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r) →
tsupport (backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r) ⊆
euclideanClosedBall x₀ (3 * ρ / 4) ×ˢ Set.Icc (t₀ - ρ ^ 2) (t₀ + ε)
theorem
CKN.caccioppoli_I1_heat_cutoff_raw_ne_top
{Ω : 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)
:
∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 2 * ENNReal.ofReal
|timePartial
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r w)
z + ∑ i : Fin 3,
spatialSecondPartial
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r w)
i i z| ≠ ⊤
theorem
CKN.caccioppoli_I2_heat_cutoff_raw_ne_top
{Ω : 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)
{c : Foundation.Parabolic.ParabolicPoint → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ ε r : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
(hr : 0 < r)
(hscale : r ≤ ρ / 2)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
(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₀ ρ)))
(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₀) ρ))
(hvelocity :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≠ ⊤)
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal |Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 2 - c w| * ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) * ENNReal.ofReal
(∑ i : Fin 3,
|spatialPartial
(fun (y : Foundation.Parabolic.ParabolicPoint) =>
backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r y)
i w|) ≠ ⊤
theorem
CKN.caccioppoli_I3_heat_cutoff_raw_ne_top
{Ω : 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)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
(hvelocity :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≠ ⊤)
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, 2 * ENNReal.ofReal |p w| * ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) * ENNReal.ofReal
(∑ i : Fin 3,
|spatialPartial
(fun (y : Foundation.Parabolic.ParabolicPoint) =>
backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r y)
i w|) ≠ ⊤
theorem
CKN.caccioppoli_I4_heat_cutoff_raw_ne_top
{Ω : 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)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
(hvelocity :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≠ ⊤)
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, 2 * ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) * ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) * ENNReal.ofReal (backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r w) ≠ ⊤