AELocal Energy

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.localEnergyRhs_eq_zero_of_not_mem_tsupport_public {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.Vec3 × ℝ → ℝ} {f : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport ψ) : localEnergyRhs u p f ψ z = 0

theorem CKN.suitableWeakSolution_energy_integrable {Ω : 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) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialGradientSq u Du z * ψ z) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => localEnergyRhs u p f ψ z) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * ψ z) MeasureTheory.volume

theorem CKN.suitableWeakSolution_localEnergyInequality_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)

The local energy inequality for almost every time slice.