The integrand of the weak momentum identity

The weak momentum clause of def:sws pairs an identity with an integrability side condition on its integrand, stated on the closed support of the vector-valued test field φ. The integrand has five terms: the time derivative term uᵢ ∂ₜφᵢ, the nonlinear term uᵢ uⱼ ∂ⱼφᵢ, the viscous term Duᵢⱼ ∂ⱼφᵢ, the pressure term p ∂ᵢφᵢ and the force term fᵢ φᵢ.

This file proves that side condition from the data clauses alone. The closed support is compact, so Lebesgue measure restricted to it is finite; on a finite measure every exponent above 1 is integrable, and a product of two square integrable factors is integrable by the Cauchy-Schwarz inequality. That is all the nonlinear term needs: no parabolic interpolation enters here, because the test field confines the integral to a set of finite measure. Each term is then an integrable field times a bounded derivative of the test field.

Nothing about the identities of def:sws is used, so the conclusion is available while those identities are still being established.

Components of a vector-valued test field

theorem CKN.component_mem_spaceTimeTestFunction {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Ω I) (i : Fin 3) : (fun (w : Foundation.Parabolic.Vec3 × ℝ) => φ w i) ∈ spaceTimeTestFunction Ω I

Each component of a vector-valued space-time test field is a scalar space-time test field on the same carrier.

The fields of the momentum integrand on a compact set

theorem CKN.velocity_pair_integrableOn_compact_of_data {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {K : Set Foundation.Parabolic.ParabolicPoint} (hdata : IsSuitableWeakSolutionData Ω I q u Du p f) (hK : IsCompact K) (hKsub : K ⊆ spaceTimeSet Ω I) (i j : Fin 3) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i * u z j) K MeasureTheory.volume

A product of two velocity components is integrable on a compact subset of the carrier: both factors are square integrable there, and the Cauchy-Schwarz inequality pairs the exponents 2 and 2 into 1.

theorem CKN.gradient_entry_integrableOn_compact_of_data {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {K : Set Foundation.Parabolic.ParabolicPoint} (hdata : IsSuitableWeakSolutionData Ω I q u Du p f) (hK : IsCompact K) (hKsub : K ⊆ spaceTimeSet Ω I) (i j : Fin 3) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) K MeasureTheory.volume

Each entry of the velocity gradient is integrable on a compact subset of the carrier.

theorem CKN.pressure_integrableOn_compact_of_data {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {K : Set Foundation.Parabolic.ParabolicPoint} (hdata : IsSuitableWeakSolutionData Ω I q u Du p f) (hK : IsCompact K) (hKsub : K ⊆ spaceTimeSet Ω I) : MeasureTheory.IntegrableOn p K MeasureTheory.volume

The pressure is integrable on a compact subset of the carrier: it is L^{3/2} there and the restricted measure is finite.

theorem CKN.force_component_integrableOn_compact_of_data {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {K : Set Foundation.Parabolic.ParabolicPoint} (hdata : IsSuitableWeakSolutionData Ω I q u Du p f) (hK : IsCompact K) (hKsub : K ⊆ spaceTimeSet Ω I) (i : Fin 3) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => f z i) K MeasureTheory.volume

Each component of the force is integrable on a compact subset of the carrier: it is L^q there with q > 5 / 2 > 1, and the restricted measure is finite.

The five terms of the momentum integrand

theorem CKN.momentum_timeTerm_integrableOn_of_data {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {K : Set Foundation.Parabolic.ParabolicPoint} (hdata : IsSuitableWeakSolutionData Ω I q u Du p f) (hK : IsCompact K) (hKsub : K ⊆ spaceTimeSet Ω I) {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Ω I) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, u z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z) K MeasureTheory.volume

The time-derivative term of the momentum integrand is integrable on a compact subset of the carrier.

theorem CKN.momentum_nonlinearTerm_integrableOn_of_data {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {K : Set Foundation.Parabolic.ParabolicPoint} (hdata : IsSuitableWeakSolutionData Ω I q u Du p f) (hK : IsCompact K) (hKsub : K ⊆ spaceTimeSet Ω I) {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Ω I) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z) K MeasureTheory.volume

The nonlinear term of the momentum integrand is integrable on a compact subset of the carrier.

theorem CKN.momentum_viscousTerm_integrableOn_of_data {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {K : Set Foundation.Parabolic.ParabolicPoint} (hdata : IsSuitableWeakSolutionData Ω I q u Du p f) (hK : IsCompact K) (hKsub : K ⊆ spaceTimeSet Ω I) {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Ω I) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z) K MeasureTheory.volume

The viscous term of the momentum integrand is integrable on a compact subset of the carrier.

theorem CKN.momentum_pressureTerm_integrableOn_of_data {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {K : Set Foundation.Parabolic.ParabolicPoint} (hdata : IsSuitableWeakSolutionData Ω I q u Du p f) (hK : IsCompact K) (hKsub : K ⊆ spaceTimeSet Ω I) {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Ω I) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => p z * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z) K MeasureTheory.volume

The pressure term of the momentum integrand is integrable on a compact subset of the carrier.

theorem CKN.momentum_forceTerm_integrableOn_of_data {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {K : Set Foundation.Parabolic.ParabolicPoint} (hdata : IsSuitableWeakSolutionData Ω I q u Du p f) (hK : IsCompact K) (hKsub : K ⊆ spaceTimeSet Ω I) {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Ω I) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, f z i * φ z i) K MeasureTheory.volume

The force term of the momentum integrand is integrable on a compact subset of the carrier.

The momentum integrand

theorem CKN.momentum_integrand_integrableOn_of_data {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hdata : IsSuitableWeakSolutionData Ω I q u Du p f) {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Ω I) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => -∑ i : Fin 3, u z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z - p z * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z - ∑ i : Fin 3, f z i * φ z i) (tsupport φ) MeasureTheory.volume

The integrand of the weak momentum clause of def:sws is integrable on the closed support of the test field. Only the data clauses are used.