Local Energy Mollified Data

Supporting estimates for the Navier–Stokes development.

theorem CKN.localEnergy_memLp_parabolic_to_product {E : Type} [NormedAddCommGroup E] {f : Foundation.Parabolic.ParabolicPoint → E} {p : ENNReal} (hf : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => f z) p (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0))

Transfer a space-time MemLp bound from the parabolic coordinate carrier to the product coordinate carrier.

theorem CKN.essLocal_mollifiedMomentumWeak_of_essLocalData {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} (hS3 : ∀ φ ∈ spaceTimeTestFunction (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), -∑ i : Fin 3, u z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφU : tsupport φ ⊆ Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), mollifiedMomentumWeakIntegrand (fun (y : Foundation.Parabolic.Vec3 × ℝ) => (Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator u y) (fun (y : Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) => (Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator (fun (q : Foundation.Parabolic.Vec3 × ℝ) => u q i * u q j) y) (fun (y : Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) => (Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator (fun (q : Foundation.Parabolic.Vec3 × ℝ) => Du q i j) y) (fun (y : Foundation.Parabolic.Vec3 × ℝ) => (Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator p y) φ z = 0

The E1 momentum identity, extended by zero, remains a global weak identity for compactly supported tests in the unit cylinder.

theorem CKN.essLocal_mollifiedDivergenceWeak_of_essLocalData {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hS2 : ∀ ψ ∈ spaceTimeTestFunction (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∑ i : Fin 3, u z i * spatialPartial ψ i z = 0) (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, (Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator u z i * (fderiv ℝ ψ z) (energySpatialDir i) = 0

The E1 divergence identity, extended by zero, remains a global weak identity for compactly supported tests in the unit cylinder.

theorem CKN.essLocal_mollifiedMomentumEquation_of_essLocalData {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (henergy : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (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 (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hS2 : ∀ ψ ∈ spaceTimeTestFunction (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∑ i : Fin 3, u z i * spatialPartial ψ i z = 0) (hS3 : ∀ φ ∈ spaceTimeTestFunction (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), -∑ i : Fin 3, u z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) {δ : ℝ} (hδ : 0 < δ) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : Metric.closedBall z δ ⊆ Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0) : (∀ (i : Fin 3), (fderiv ℝ (spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => (Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator u y i) δ hδ) z) energyTimeDir + ∑ j : Fin 3, (fderiv ℝ (spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => (Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator (fun (q : Foundation.Parabolic.Vec3 × ℝ) => u q i * u q j) y) δ hδ) z) (energySpatialDir j) - ∑ j : Fin 3, (fderiv ℝ (spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => (Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator (fun (q : Foundation.Parabolic.Vec3 × ℝ) => Du q i j) y) δ hδ) z) (energySpatialDir j) + (fderiv ℝ (spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => (Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator p y) δ hδ) z) (energySpatialDir i) = 0) ∧ ∑ i : Fin 3, (fderiv ℝ (spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => (Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0).indicator u y i) δ hδ) z) (energySpatialDir i) = 0

The E1 momentum identity gives the pointwise equation for local mollifications of the zero-extended fields.