Point tests of the momentum identity

For a fixed spatial point x, a direction k and a smooth time test θ, the space-time field θ(t) η(x - y) e_k is an admissible test of eq:reg-momentum-forced. Its time and spatial derivatives are explicit, and the momentum integrand splits into the time derivative of the test times the velocity and the test times an explicit kernel. This is the first step of the local energy inequality eq:reg-local-energy-forced.

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

The point test θ(t) η(x - y) e_k.

Equations

• CKN.Leray.lePointTest η θ x k z = (θ z.2 * η (x - z.1)) • CKN.basisVec k

theorem CKN.Leray.lePointTest_contDiff {η : Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (x : Foundation.Parabolic.Vec3) (k : Fin 3) (hη : ContDiff ℝ (↑⊤) η) (hθ : ContDiff ℝ (↑⊤) θ) : ContDiff ℝ (↑⊤) (lePointTest η θ x k)

theorem CKN.Leray.lePointTest_support_subset {η : Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (x : Foundation.Parabolic.Vec3) (k : Fin 3) : Function.support (lePointTest η θ x k) ⊆ ((fun (y : Foundation.Parabolic.Vec3) => x - y) '' tsupport η) ×ˢ tsupport θ

theorem CKN.Leray.lePointTest_hasCompactSupport {η : Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (x : Foundation.Parabolic.Vec3) (k : Fin 3) (hηc : HasCompactSupport η) (hθc : HasCompactSupport θ) : HasCompactSupport (lePointTest η θ x k)

theorem CKN.Leray.lePointTest_tsupport {η : Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (x : Foundation.Parabolic.Vec3) (k : Fin 3) (hηc : HasCompactSupport η) (hθc : HasCompactSupport θ) {T : ℝ} (hθs : tsupport θ ⊆ Set.Ioo 0 T) (z : Foundation.Parabolic.Vec3 × ℝ) : z ∈ tsupport (lePointTest η θ x k) → z.2 ∈ Set.Ioo 0 T

theorem CKN.Leray.hasFDerivAt_lePointTest_scalar {η : Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (x : Foundation.Parabolic.Vec3) (hη : ContDiff ℝ (↑⊤) η) (hθ : ContDiff ℝ (↑⊤) θ) (z : Foundation.Parabolic.Vec3 × ℝ) : HasFDerivAt (fun (w : Foundation.Parabolic.Vec3 × ℝ) => θ w.2 * η (x - w.1)) (θ z.2 • fderiv ℝ η (x - z.1) ∘SL (-ContinuousLinearMap.fst ℝ Foundation.Parabolic.Vec3 ℝ) + η (x - z.1) • fderiv ℝ θ z.2 ∘SL ContinuousLinearMap.snd ℝ Foundation.Parabolic.Vec3 ℝ) z

theorem CKN.Leray.timeDeriv_lePointTest {η : Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (x : Foundation.Parabolic.Vec3) (k : Fin 3) (hη : ContDiff ℝ (↑⊤) η) (hθ : ContDiff ℝ (↑⊤) θ) (z : Foundation.Parabolic.Vec3 × ℝ) : timeDeriv (lePointTest η θ x k) z = (deriv θ z.2 * η (x - z.1)) • basisVec k

theorem CKN.Leray.spaceDeriv_lePointTest {η : Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (x : Foundation.Parabolic.Vec3) (k : Fin 3) (hη : ContDiff ℝ (↑⊤) η) (hθ : ContDiff ℝ (↑⊤) θ) (j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spaceDeriv j (lePointTest η θ x k) z = -(θ z.2 * spatialDeriv η j (x - z.1)) • basisVec k

theorem CKN.Leray.sum_sum_ite_eq_fin (k : Fin 3) (A : Fin 3 → Fin 3 → ℝ) : (∑ i : Fin 3, ∑ j : Fin 3, if i = k then A i j else 0) = ∑ j : Fin 3, A k j

noncomputable def CKN.Leray.leKernel (ρ : 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.

Equations

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

theorem CKN.Leray.forcedMomentumIntegrand_lePointTest (ρ : 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θ : ContDiff ℝ (↑⊤) θ) (x : Foundation.Parabolic.Vec3) (k : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : forcedMomentumIntegrand ρ ε hε ha f hf (lePointTest η θ x k) z = -(deriv θ z.2 * (η (x - z.1) * forcedRegRep ρ ε hε ha hf z k)) + θ z.2 * leKernel ρ ε hε ha f hf η x k z