Local Energy Mollified Momentum

Supporting estimates for the Navier–Stokes development.

theorem CKN.localEnergyMollifiedVolumeIsAddHaarMeasure : MeasureTheory.volume.IsAddHaarMeasure

noncomputable def CKN.translatedMollifier (z : Foundation.Parabolic.Vec3 × ℝ) (δ : ℝ) (hδ : 0 < δ) : Foundation.Parabolic.Vec3 × ℝ → ℝ

The space-time mollifier reflected and translated to the point z.

Equations

• CKN.translatedMollifier z δ hδ y = CKN.spaceTimeMollifier δ hδ (z - y)

noncomputable def CKN.mollifierVectorTest (z : Foundation.Parabolic.Vec3 × ℝ) (i : Fin 3) (δ : ℝ) (hδ : 0 < δ) : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3

A vector test with the translated space-time mollifier in coordinate i.

Equations

• CKN.mollifierVectorTest z i δ hδ y = Pi.single i (CKN.translatedMollifier z δ hδ y)

def CKN.energyTimeDir : Foundation.Parabolic.Vec3 × ℝ

The unit direction in the time coordinate of product spacetime.

Equations

• CKN.energyTimeDir = (0, 1)

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

The unit direction in the jth spatial coordinate of product spacetime.

Equations

• CKN.energySpatialDir j = (CKN.basisVec j, 0)

noncomputable def CKN.energyDirDeriv (f : Foundation.Parabolic.Vec3 × ℝ → ℝ) (v z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The derivative of a scalar spacetime function in a fixed direction.

Equations

• CKN.energyDirDeriv f v z = (fderiv ℝ f z) v

noncomputable def CKN.mollifiedMomentumWeakIntegrand (u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (F G : Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ) (p : Foundation.Parabolic.Vec3 × ℝ → ℝ) (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The weak momentum integrand used to pass the local equation through a mollifier.

Equations

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

theorem CKN.spaceTimeMollify_momentum_fderiv_of_weak {U : Set (Foundation.Parabolic.Vec3 × ℝ)} {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {F G : Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ} {p : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hweak : ∀ (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → ∫ (z : Foundation.Parabolic.Vec3 × ℝ), mollifiedMomentumWeakIntegrand u F G p φ z = 0) (hu : ∀ (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u z i) MeasureTheory.volume) (hF : ∀ (i j : Fin 3), MeasureTheory.LocallyIntegrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => F z i j) MeasureTheory.volume) (hG : ∀ (i j : Fin 3), MeasureTheory.LocallyIntegrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => G z i j) MeasureTheory.volume) (hp : MeasureTheory.LocallyIntegrable p MeasureTheory.volume) {δ : ℝ} (hδ : 0 < δ) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : Metric.closedBall z δ ⊆ U) (i : Fin 3) : (fderiv ℝ (spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => u y i) δ hδ) z) energyTimeDir + ∑ j : Fin 3, (fderiv ℝ (spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => F y i j) δ hδ) z) (energySpatialDir j) - ∑ j : Fin 3, (fderiv ℝ (spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => G y i j) δ hδ) z) (energySpatialDir j) + (fderiv ℝ (spaceTimeMollify p δ hδ) z) (energySpatialDir i) = 0

A distributional momentum identity convolved by the space-time kernel gives the smooth momentum equation in every ball on which the kernel stays inside the testing domain.

theorem CKN.spaceTimeMollify_divergence_eq_zero_of_weak {U : Set (Foundation.Parabolic.Vec3 × ℝ)} {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hweak : ∀ (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ U → ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, u z i * (fderiv ℝ ψ z) (energySpatialDir i) = 0) (hu : ∀ (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u z i) MeasureTheory.volume) {δ : ℝ} (hδ : 0 < δ) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : Metric.closedBall z δ ⊆ U) : ∑ i : Fin 3, (fderiv ℝ (spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => u y i) δ hδ) z) (energySpatialDir i) = 0

A weakly divergence-free locally integrable velocity remains divergence free after local space-time mollification.