The weak time derivative of the mollified velocity

At every spatial point x, the spatial mollification ∫ η(x - y) u(y, t) dy of the forced regularized velocity is continuous in time and has weak time derivative -∫ K(x; y, t) dy, where K is the kernel of the point-tested momentum identity eq:reg-momentum-forced. This is the time regularity used in the local energy inequality eq:reg-local-energy-forced.

noncomputable def CKN.Leray.leW (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (η : Foundation.Parabolic.Vec3 → ℝ) (x : Foundation.Parabolic.Vec3) (t : ℝ) (k : Fin 3) : ℝ

The mollified velocity at a point.

Equations

• CKN.Leray.leW ρ ε hε ha hf η x t k = ∫ (y : CKN.Foundation.Parabolic.Vec3), η (x - y) * CKN.Leray.forcedRegRep ρ ε hε ha hf (y, t) k

noncomputable def CKN.Leray.leS (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (η : Foundation.Parabolic.Vec3 → ℝ) (x : Foundation.Parabolic.Vec3) (t : ℝ) (k : Fin 3) : ℝ

The source of the mollified velocity at a point.

Equations

• CKN.Leray.leS ρ ε hε ha hf η x t k = ∫ (y : CKN.Foundation.Parabolic.Vec3), CKN.Leray.leKernel ρ ε hε ha f hf η x k (y, t)

def CKN.Leray.lePointField (η : Foundation.Parabolic.Vec3 → ℝ) (x : Foundation.Parabolic.Vec3) (k : Fin 3) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The point field η(x - ·) e_k.

Equations

• CKN.Leray.lePointField η x k y = η (x - y) • CKN.basisVec k

theorem CKN.Leray.memLp_lePointField {η : Foundation.Parabolic.Vec3 → ℝ} (hη : Continuous η) (hηc : HasCompactSupport η) (x : Foundation.Parabolic.Vec3) (k : Fin 3) : MeasureTheory.MemLp (lePointField η x k) 2 MeasureTheory.volume

theorem CKN.Leray.leW_eq_inner (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {η : Foundation.Parabolic.Vec3 → ℝ} (hη : Continuous η) (hηc : HasCompactSupport η) (x : Foundation.Parabolic.Vec3) (t : ℝ) (k : Fin 3) : leW ρ ε hε ha hf η x t k = inner ℝ (forcedRegCurve ρ ε hε ha hf t) (realVectorL2OfCoordinateFunction (lePointField η x k) ⋯)

theorem CKN.Leray.continuous_leW (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {η : Foundation.Parabolic.Vec3 → ℝ} (hη : Continuous η) (hηc : HasCompactSupport η) (x : Foundation.Parabolic.Vec3) (k : Fin 3) : Continuous fun (t : ℝ) => leW ρ ε hε ha hf η x t k

theorem CKN.Leray.hasWeakDerivOn_leW (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {η : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (x : Foundation.Parabolic.Vec3) (k : Fin 3) {T : ℝ} (hT : 0 < T) : HasWeakDerivOn (Set.Ioo 0 T) (fun (t : ℝ) => leW ρ ε hε ha hf η x t k) fun (t : ℝ) => -leS ρ ε hε ha hf η x t k

The weak time derivative of the mollified velocity at a point.