Pointwise Energy

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

noncomputable def CKN.timePartialProd (g : Foundation.Parabolic.Vec3 × ℝ → ℝ) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The time derivative on the explicit space-time product carrier.

Equations

• CKN.timePartialProd g z = CKN.timePartial (have this := g; this) z

noncomputable def CKN.spatialPartialProd (g : Foundation.Parabolic.Vec3 × ℝ → ℝ) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The spatial derivative on the explicit space-time product carrier.

Equations

• CKN.spatialPartialProd g i z = CKN.spatialPartial (have this := g; this) i z

noncomputable def CKN.spatialSecondPartialProd (g : Foundation.Parabolic.Vec3 × ℝ → ℝ) (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The iterated spatial derivative on the explicit product carrier.

Equations

• CKN.spatialSecondPartialProd g i j z = CKN.spatialSecondPartial (have this := g; this) i j z

noncomputable def CKN.localEnergyRhs (u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.Vec3 × ℝ → ℝ) (f : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The right-hand energy density in the local energy inequality.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.suitableWeakSolution_energyInequality {Ω : 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) : 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, spatialGradientSq u Du z * ψ z ≤ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, localEnergyRhs u p f ψ z

The suitable-solution energy inequality, with its density named.