Local Energy Mollified Energy

Local energy identities and limit passages for the endpoint regularity proof.

theorem ESS.localEnergyHolderTripleFourFourTwo : ENNReal.HolderTriple 4 4 2

def ESS.localEnergySpatialDir (j : Fin 3) : CKN.Foundation.Parabolic.Vec3 × ℝ

The product-space direction corresponding to the jth spatial coordinate.

Equations

• ESS.localEnergySpatialDir j = (CKN.basisVec j, 0)

theorem ESS.localEnergy_tendsto_eLpNorm_mul_sub {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q r : ENNReal} [htriple : p.HolderTriple q r] (hr : 1 ≤ r) {f g : α → ℝ} (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g q μ) {fn gn : ℕ → α → ℝ} (hfn : ∀ (n : ℕ), MeasureTheory.MemLp (fn n) p μ) (hgn : ∀ (n : ℕ), MeasureTheory.MemLp (gn n) q μ) (hfnLim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => fn n x - f x) p μ) Filter.atTop (nhds 0)) (hgnLim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => gn n x - g x) q μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => fn n x * gn n x - f x * g x) r μ) Filter.atTop (nhds 0)

Products converge in the Hölder exponent when both factors converge in their respective Lebesgue norms.

theorem ESS.localEnergy_mollified_base_integral_zero {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (henergy : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤) (hpLp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hL3 : essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3) (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤) (hgrad : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (i : Fin 3), CKN.HasWeakGradientOn (CKN.Foundation.Parabolic.vec3Ball 0 1) (fun (x : CKN.Vec 3) => u (x, t) i) fun (x : CKN.Vec 3) => Du (x, t) i) (hS2 : ∀ ψ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∑ i : Fin 3, u z i * CKN.spatialPartial ψ i z = 0) (hS3 : ∀ φ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) {δ : ℝ} (hδ : 0 < δ) (hcover : ∀ z ∈ tsupport ψ, Metric.closedBall z (3 * δ) ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), smoothEnergyBaseIntegrand (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) (i : Fin 3) => CKN.spaceTimeMollify ((CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => u q i) δ hδ y) (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) => CKN.spaceTimeMollify ((CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => u q i * u q j) δ hδ y - CKN.spaceTimeMollify ((CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => u q i) δ hδ y * CKN.spaceTimeMollify ((CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => u q j) δ hδ y) (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) => CKN.spaceTimeMollify ((CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => Du q i j) δ hδ y) (CKN.spaceTimeMollify ((CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator p) δ hδ) ψ z = 0

A compactly supported smooth energy test has zero mollified energy density on every interior scale for which its support stays inside the unit cylinder.