Local Energy Equality

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

theorem ESS.localEnergyEqualityHolderTripleFourFourTwo : ENNReal.HolderTriple 4 4 2

theorem ESS.localEnergyEqualityHolderTripleTwoFourFourThree : ENNReal.HolderTriple 2 4 (ENNReal.ofReal (4 / 3))

theorem ESS.localEnergyEqualityHolderTripleThreeTwoFourTwelveEleven : (ENNReal.ofReal (3 / 2)).HolderTriple 4 (ENNReal.ofReal (12 / 11))

theorem ESS.localEnergyEqualityHolderTripleTwoTwoOne : ENNReal.HolderTriple 2 2 1

def ESS.localEnergyUnitProductCylinder : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)

The ordinary product-space carrier for the unit backward cylinder.

Equations

• ESS.localEnergyUnitProductCylinder = CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0

noncomputable def ESS.localEnergyVelocityZeroExtension (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (i : Fin 3) : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The componentwise zero extension of the velocity from the unit cylinder.

Equations

• ESS.localEnergyVelocityZeroExtension u i = ESS.localEnergyUnitProductCylinder.indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i

noncomputable def ESS.localEnergyTensorZeroExtension (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (i j : Fin 3) : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The componentwise zero extension of the quadratic velocity tensor.

Equations

• ESS.localEnergyTensorZeroExtension u i j = ESS.localEnergyUnitProductCylinder.indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i * u z j

noncomputable def ESS.localEnergyGradientZeroExtension (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (i j : Fin 3) : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The componentwise zero extension of the weak gradient.

Equations

• ESS.localEnergyGradientZeroExtension Du i j = ESS.localEnergyUnitProductCylinder.indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Du z i j

noncomputable def ESS.localEnergyPressureZeroExtension (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The zero extension of the pressure from the unit cylinder.

Equations

• ESS.localEnergyPressureZeroExtension p = ESS.localEnergyUnitProductCylinder.indicator p

noncomputable def ESS.localEnergyMollifiedVelocity (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (δ : ℝ) (hδ : 0 < δ) : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3

The smooth space-time mollification of a velocity component zero extension.

Equations

• ESS.localEnergyMollifiedVelocity u δ hδ z i = CKN.spaceTimeMollify (ESS.localEnergyVelocityZeroExtension u i) δ hδ z

noncomputable def ESS.localEnergyMollifiedTensor (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (δ : ℝ) (hδ : 0 < δ) : CKN.Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ

The smooth space-time mollification of a quadratic velocity tensor component.

Equations

• ESS.localEnergyMollifiedTensor u δ hδ z i j = CKN.spaceTimeMollify (ESS.localEnergyTensorZeroExtension u i j) δ hδ z

noncomputable def ESS.localEnergyMollifiedGradient (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (δ : ℝ) (hδ : 0 < δ) : CKN.Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ

The smooth space-time mollification of a weak-gradient component.

Equations

• ESS.localEnergyMollifiedGradient Du δ hδ z i j = CKN.spaceTimeMollify (ESS.localEnergyGradientZeroExtension Du i j) δ hδ z

noncomputable def ESS.localEnergyMollifiedPressure (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (δ : ℝ) (hδ : 0 < δ) : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The smooth space-time mollification of the pressure zero extension.

Equations

• ESS.localEnergyMollifiedPressure p δ hδ = CKN.spaceTimeMollify (ESS.localEnergyPressureZeroExtension p) δ hδ

theorem ESS.localEnergy_tendsto_eLpNorm_finset_sum_sub {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} (hp : 1 ≤ p) {ι : Type u_2} (s : Finset ι) (fn : ℕ → ι → α → ℝ) (f : ι → α → ℝ) (hconv : ∀ i ∈ s, Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => fn n i x - f i x) p μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => ∑ i ∈ s, fn n i x - ∑ i ∈ s, f i x) p μ) Filter.atTop (nhds 0)

Finite sums preserve convergence in an Lᵖ seminorm when p ≥ 1.

theorem ESS.localEnergy_mollify_memLp {g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {p : ENNReal} {δr : ℝ} (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hδ : 0 < δr) (hg : MeasureTheory.MemLp g p MeasureTheory.volume) : MeasureTheory.MemLp (CKN.spaceTimeMollify g δr hδ) p MeasureTheory.volume

Space-time mollification preserves finite-exponent MemLp membership.

theorem ESS.localEnergy_testCoefficients {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.timePartial ψ z + ∑ i : Fin 3, CKN.spatialSecondPartial ψ i i z) 2 MeasureTheory.volume ∧ (∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial ψ i z) 4 MeasureTheory.volume) ∧ (∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial ψ i z) 12 MeasureTheory.volume) ∧ MeasureTheory.MemLp ψ ⊤ MeasureTheory.volume

Smooth compactly supported energy-test coefficients have the exponents needed for the space-time Hölder pairings in the energy identity.

theorem ESS.localEnergy_tendsto_eLpNorm_add_sub {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} (hp : 1 ≤ p) {f g : α → ℝ} {fn gn : ℕ → α → ℝ} (hfn : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => fn n x - f x) p μ) Filter.atTop (nhds 0)) (hgn : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => gn n x - g x) p μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => fn n x + gn n x - (f x + g x)) p μ) Filter.atTop (nhds 0)

Sums of two convergent sequences converge in an Lᵖ seminorm when p ≥ 1.

theorem ESS.localEnergy_zeroExtensionLp {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) : (∀ (i : Fin 3), MeasureTheory.MemLp ((CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i) 4 MeasureTheory.volume) ∧ (∀ (i j : Fin 3), MeasureTheory.MemLp ((CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i * u z j) 2 MeasureTheory.volume) ∧ (∀ (i j : Fin 3), MeasureTheory.MemLp ((CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Du z i j) 2 MeasureTheory.volume) ∧ MeasureTheory.MemLp ((CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator p) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

The unit-cylinder zero extensions have the Lebesgue integrability needed for mollification.

theorem ESS.localEnergy_exists_scales_for_test {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0) : ∃ (ε : ℝ), 0 < ε ∧ ∃ (δ : ℕ → ℝ), Filter.Tendsto δ Filter.atTop (nhds 0) ∧ (∀ (n : ℕ), 0 < δ n) ∧ ∀ (n : ℕ), ∀ z ∈ tsupport ψ, Metric.closedBall z (3 * δ n) ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0

A compactly supported test admits positive mollifier scales whose convolution neighborhoods stay within the unit cylinder.

theorem ESS.localEnergy_mollifiedInputs_tendsto {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) {δ : ℕ → ℝ} (hδ : Filter.Tendsto δ Filter.atTop (nhds 0)) (hδpos : ∀ (n : ℕ), 0 < δ n) : (∀ (i : Fin 3), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spaceTimeMollify ((CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => u q i) (δ n) ⋯ z - (CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => u q i) z) 4 MeasureTheory.volume) Filter.atTop (nhds 0)) ∧ (∀ (i j : Fin 3), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => 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) (δ n) ⋯ z - (CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => u q i * u q j) z) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) ∧ (∀ (i j : Fin 3), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spaceTimeMollify ((CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => Du q i j) (δ n) ⋯ z - (CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => Du q i j) z) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spaceTimeMollify ((CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator p) (δ n) ⋯ z - (CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator p z) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) Filter.atTop (nhds 0)

The scalar zero extensions converge to their mollifications in the exponents used by the local energy identity.

theorem ESS.localEnergy_mollifiedProducts_tendsto {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) {δ : ℕ → ℝ} (hδ : Filter.Tendsto δ Filter.atTop (nhds 0)) (hδpos : ∀ (n : ℕ), 0 < δ n) : (∀ (i : Fin 3), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => localEnergyMollifiedVelocity u (δ n) ⋯ z i * localEnergyMollifiedVelocity u (δ n) ⋯ z i - localEnergyVelocityZeroExtension u i z * localEnergyVelocityZeroExtension u i z) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) ∧ (∀ (i j : Fin 3), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => localEnergyMollifiedVelocity u (δ n) ⋯ z i * localEnergyMollifiedVelocity u (δ n) ⋯ z i * localEnergyMollifiedVelocity u (δ n) ⋯ z j - localEnergyVelocityZeroExtension u i z * localEnergyVelocityZeroExtension u i z * localEnergyVelocityZeroExtension u j z) (ENNReal.ofReal (4 / 3)) MeasureTheory.volume) Filter.atTop (nhds 0)) ∧ (∀ (i : Fin 3), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => localEnergyMollifiedPressure p (δ n) ⋯ z * localEnergyMollifiedVelocity u (δ n) ⋯ z i - localEnergyPressureZeroExtension p z * localEnergyVelocityZeroExtension u i z) (ENNReal.ofReal (12 / 11)) MeasureTheory.volume) Filter.atTop (nhds 0)) ∧ (∀ (i j : Fin 3), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => localEnergyMollifiedTensor u (δ n) ⋯ z i j - localEnergyMollifiedVelocity u (δ n) ⋯ z i * localEnergyMollifiedVelocity u (δ n) ⋯ z j) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) ∧ ∀ (i j : Fin 3), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => localEnergyMollifiedGradient Du (δ n) ⋯ z i j * localEnergyMollifiedGradient Du (δ n) ⋯ z i j - localEnergyGradientZeroExtension Du i j z * localEnergyGradientZeroExtension Du i j z) 1 MeasureTheory.volume) Filter.atTop (nhds 0)

Products of the mollified velocity, stress, gradient, and pressure converge in the Lebesgue exponents used by the local energy identity.