The source of the mollified velocity

The kernel of the point-tested momentum identity is written with the strongly measurable modification of the force, which changes the source only on a null set of times. The resulting source is jointly measurable, and on almost every time slice it is a sum of convolutions of square-integrable fields with the mollifier and its derivatives, bounded uniformly in space by an integrable function of time. These are the ingredients of the local energy inequality eq:reg-local-energy-forced.

noncomputable def CKN.Leray.leTensor (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (j k : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The transport-minus-viscous tensor of the forced regularized solution.

Equations

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

noncomputable def CKN.Leray.lePressure (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The pressure of the forced regularized solution as a space-time field.

Equations

• CKN.Leray.lePressure ρ ε hε ha hf z = CKN.Leray.forcedQuadPressure ρ ε hε (CKN.Leray.forcedRegCurve ρ ε hε ha hf) z + CKN.Leray.forcePressure f hf z

noncomputable def CKN.Leray.leKernelF (ρ : 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) (k : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The kernel of the point-tested momentum identity with the modified force.

Equations

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

noncomputable def CKN.Leray.leSF (ρ : 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 with the modified force.

Equations

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

theorem CKN.Leray.ae_leS_eq_leSF (ρ : 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 → ℝ) {T : ℝ} (hT : 0 < T) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (x : Foundation.Parabolic.Vec3) (k : Fin 3), leS ρ ε hε ha hf η x t k = leSF ρ ε hε ha hf η x t k

theorem CKN.Leray.hasWeakDerivOn_leW_F (ρ : 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 : ℝ) => -leSF ρ ε hε ha hf η x t k

The weak time derivative of the mollified velocity with the modified source.