Caccioppoli Energy Tools #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.caccioppoli_timePartial_zero_of_not_mem_tsupport
{F : Foundation.Parabolic.Vec3 × ℝ → ℝ}
:
ContDiff ℝ (↑⊤) F → ∀ {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport F), timePartial F z = 0
theorem
CKN.caccioppoli_spatialPartial_zero_of_not_mem_tsupport
{F : Foundation.Parabolic.Vec3 × ℝ → ℝ}
:
ContDiff ℝ (↑⊤) F → ∀ {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport F) (i : Fin 3), spatialPartial F i z = 0
theorem
CKN.caccioppoli_terms_zero_ae_outside_cylinder
{Ω : Set Foundation.Parabolic.Vec3}
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ ε : ℝ}
(hρ : 0 < ρ)
(hΩ : MeasurableSet Ω)
{F : Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hF : ContDiff ℝ (↑⊤) F)
(hFsupp : tsupport F ⊆ euclideanClosedBall x₀ (3 * ρ / 4) ×ˢ Set.Icc (t₀ - ρ ^ 2) (t₀ + ε))
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{t : ℝ}
(ht : t ≤ t₀)
:
∀ᵐ (z : Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (Ω ×ˢ Set.Iio t), z ∈ Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ ∨ Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (timePartial F z + ∑ i : Fin 3, spatialSecondPartial F i i z) = 0 ∧ Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * ∑ i : Fin 3, u z i * spatialPartial F i z = 0 ∧ 2 * (p z - 0) * ∑ i : Fin 3, u z i * spatialPartial F i z = 0 ∧ (2 * ∑ i : Fin 3, f z i * u z i) * F z = 0 ∧ ∑ i : Fin 3, u z i * spatialPartial F i z = 0
theorem
CKN.caccioppoli_integrable_of_lintegral_abs_ne_top
{Q : Set Foundation.Parabolic.ParabolicPoint}
{g : Foundation.Parabolic.ParabolicPoint → ℝ}
(hg : AEMeasurable g (MeasureTheory.volume.restrict Q))
(hfin : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Q, ENNReal.ofReal |g z| ≠ ⊤)
:
theorem
CKN.caccioppoli_integral_term_le_raw
{S Q : Set Foundation.Parabolic.ParabolicPoint}
{g : Foundation.Parabolic.ParabolicPoint → ℝ}
(hS : MeasurableSet S)
:
MeasurableSet Q →
∀ (hg : MeasureTheory.IntegrableOn g Q MeasureTheory.volume)
(hzero : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict S, z ∈ Q ∨ g z = 0),
∫ (z : Foundation.Parabolic.ParabolicPoint) in S, g z ≤ (∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Q, ENNReal.ofReal |g z|).toReal
theorem
CKN.caccioppoli_integrable_term_on
{S Q : Set Foundation.Parabolic.ParabolicPoint}
{g : Foundation.Parabolic.ParabolicPoint → ℝ}
(hS : MeasurableSet S)
(hg : MeasureTheory.IntegrableOn g Q MeasureTheory.volume)
(hzero : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict S, z ∈ Q ∨ g z = 0)
:
theorem
CKN.caccioppoli_energy_nested_integral_eq
{Ω : Set Foundation.Parabolic.Vec3}
{T : Set ℝ}
{g : Foundation.Parabolic.ParabolicPoint → ℝ}
(hg : MeasureTheory.IntegrableOn g (Ω ×ˢ T) (MeasureTheory.volume.prod MeasureTheory.volume))
:
theorem
CKN.caccioppoli_pairing_zero_to_slice_integral
{Ω K : Set Foundation.Parabolic.Vec3}
{s : ℝ}
{F : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hK : IsCompact K)
(hKΩ : K ⊆ Ω)
(hF : ContDiff ℝ (↑⊤) F)
(hFsupp : tsupport F ⊆ K ×ˢ Set.univ)
(hUs : MeasureTheory.IntegrableOn (fun (x : Foundation.Parabolic.Vec3) => u (x, s)) K MeasureTheory.volume)
(hpair :
parametricPairing (fun (s : ℝ) (y : Foundation.Parabolic.Vec3) => F (y, s)) (fun (x : Foundation.Parabolic.Vec3) => 0)
(fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (fun (x : Foundation.Parabolic.Vec3) => 0) s = 0)
:
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, u (x, s) i * spatialPartial F i (x, s))
MeasureTheory.volume ∧ ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, u (x, s) i * spatialPartial F i (x, s) = 0
theorem
CKN.caccioppoli_rhs_integral_sum_bound
{Ω : Set Foundation.Parabolic.Vec3}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{S : Set Foundation.Parabolic.ParabolicPoint}
{T : Set ℝ}
{F : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{g₁ g₂ g₃ g₄ : Foundation.Parabolic.ParabolicPoint → ℝ}
{I₁ I₂ I₃ I₄ : ℝ}
(hR_eq :
∫ (z : Foundation.Parabolic.ParabolicPoint) in S, localEnergyRhs u p f F z = ∫ (z : Foundation.Parabolic.ParabolicPoint) in S, g₁ z + g₂ z + g₃ z + g₄ z)
(hnestR :
∫ (s : ℝ) in T, ∫ (x : Foundation.Parabolic.Vec3) in Ω, localEnergyRhs u p f F (x, s) = ∫ (z : Foundation.Parabolic.ParabolicPoint) in S, localEnergyRhs u p f F z)
(hi₁ : MeasureTheory.IntegrableOn g₁ S MeasureTheory.volume)
(hi₂ : MeasureTheory.IntegrableOn g₂ S MeasureTheory.volume)
(hi₃ : MeasureTheory.IntegrableOn g₃ S MeasureTheory.volume)
(hi₄ : MeasureTheory.IntegrableOn g₄ S MeasureTheory.volume)
(hterm₁ : ∫ (z : Foundation.Parabolic.ParabolicPoint) in S, g₁ z ≤ I₁)
(hterm₂ : ∫ (z : Foundation.Parabolic.ParabolicPoint) in S, g₂ z ≤ I₂)
(hterm₃ : ∫ (z : Foundation.Parabolic.ParabolicPoint) in S, g₃ z ≤ I₃)
(hterm₄ : ∫ (z : Foundation.Parabolic.ParabolicPoint) in S, g₄ z ≤ I₄)
: