Integrability of the momentum integrand

The regularized transport velocity of the forced regularized solution is a jointly measurable convolution, bounded on bounded time intervals. Together with the square integrability of the velocity, its gradient, the pressures and the force on bounded slabs, this makes every term of the integrand of eq:reg-momentum-forced integrable against a smooth compactly supported test.

theorem CKN.Leray.forcedRegTransport_eq (ρ : 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 × ℝ) (i : Fin 3) : regUniformMollifiedVelocity ρ ε hε (forcedRegRep ρ ε hε ha hf) z i = ∫ (y : Foundation.Parabolic.Vec3), forcedTransportKernel ρ ε hε y * forcedRegRep ρ ε hε ha hf (z.1 - y, z.2) i

The regularized transport velocity of the solution as a convolution.

theorem CKN.Leray.measurable_forcedRegTransport (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (i : Fin 3) : Measurable fun (z : Foundation.Parabolic.Vec3 × ℝ) => regUniformMollifiedVelocity ρ ε hε (forcedRegRep ρ ε hε ha hf) z i

theorem CKN.Leray.forcedRegTransport_bound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (T : ℝ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (z : Foundation.Parabolic.Vec3 × ℝ), z.2 ∈ Set.Icc 0 T → ∀ (i : Fin 3), |regUniformMollifiedVelocity ρ ε hε (forcedRegRep ρ ε hε ha hf) z i| ≤ M

The regularized transport velocity is bounded on bounded time intervals.

noncomputable def CKN.Leray.stDiv (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 × ℝ → ℝ

The spatial divergence of a space-time test.

Equations

• CKN.Leray.stDiv φ z = ∑ k : Fin 3, CKN.Leray.spaceDeriv k φ z k

theorem CKN.Leray.ae_mem_Ioo_prod (T : ℝ) : ∀ᵐ (z : Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)), z.2 ∈ Set.Ioo 0 T

theorem CKN.Leray.memLp_test_component_prod {ψ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (T : ℝ) (i : Fin 3) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => ψ z i) 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

theorem CKN.Leray.stDiv_contDiff {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) : ContDiff ℝ (↑⊤) (stDiv φ)

theorem CKN.Leray.stDiv_hasCompactSupport {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφc : HasCompactSupport φ) : HasCompactSupport (stDiv φ)

theorem CKN.Leray.memLp_forcedRegRep_prod (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (T : ℝ) : MeasureTheory.MemLp (forcedRegRep ρ ε hε ha hf) 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

theorem CKN.Leray.integrable_time_term (ρ : 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 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (T : ℝ) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => ∑ i : Fin 3, forcedRegRep ρ ε hε ha hf z i * timeDeriv φ z i) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

theorem CKN.Leray.integrable_transport_term (ρ : 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 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (T : ℝ) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε (forcedRegRep ρ ε hε ha hf) z j * forcedRegRep ρ ε hε ha hf z i * spaceDeriv j φ z i) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

theorem CKN.Leray.memLp_forcedRegGrad_prod (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (T : ℝ) (hT : 0 ≤ T) : MeasureTheory.MemLp (forcedMollifiedGrad (forcedRegRep ρ ε hε ha hf)) 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

theorem CKN.Leray.integrable_viscous_term (ρ : 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 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (T : ℝ) (hT : 0 ≤ T) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => ∑ i : Fin 3, ∑ j : Fin 3, forcedMollifiedGrad (forcedRegRep ρ ε hε ha hf) z i j * spaceDeriv j φ z i) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

theorem CKN.Leray.integrable_quadPressure_term (ρ : 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 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (T : ℝ) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => forcedQuadPressure ρ ε hε (forcedRegCurve ρ ε hε ha hf) z * stDiv φ z) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

theorem CKN.Leray.integrable_forcePressure_term {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (T : ℝ) (hT : 0 < T) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => forcePressure f hf z * stDiv φ z) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

theorem CKN.Leray.integrable_force_term {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (T : ℝ) (hT : 0 < T) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, f z i * φ z i) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))