Changing the pressure and the force by a smooth gauge

A suitable weak solution on the unit cylinder Q whose velocity is smooth and divergence free there stays suitable when the pressure π and the force f are replaced by smooth fields π' and f' with ∇π' - ∇π = f' - f on Q. The weak momentum equation and the local energy inequality change by the pairings of π' - π with div φ and with u · ∇ψ, which integration by parts on Q turns into the pairings of f' - f with φ and with u ψ. This is the form in which the averaged system of the proof of thm:main is shown to be suitable.

theorem CIV.integral_mul_spatialPartial_eq_neg {h k ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (i : Fin 3) (hh : ContDiffOn ℝ (↑⊤) h unitCylinder) (hk : ContinuousOn k unitCylinder) (hhk : ∀ z ∈ unitCylinder, CKN.spatialPartial h i z = k z) (hψ : ψ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => h z * CKN.spatialPartial ψ i z) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => k z * ψ z) MeasureTheory.volume ∧ ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), h z * CKN.spatialPartial ψ i z = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), k z * ψ z

Integration by parts in one spatial direction against a test function supported in Q, for a field smooth on Q whose partial derivative is identified there with a continuous field k.

theorem CIV.spatialPartial_sub_of_mem_unitCylinder {a b : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (ha : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => a z) unitCylinder) (hb : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => b z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (i : Fin 3) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => a w - b w) i z = CKN.spatialPartial a i z - CKN.spatialPartial b i z

The spatial partial derivative of a difference of smooth fields on Q.

theorem CIV.memLp_of_continuousOn_localBox {β : Type u_1} [NormedAddCommGroup β] {v : CKN.Foundation.Parabolic.ParabolicPoint → β} (hv : ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => v z) unitCylinder) {Ω' : Set CKN.Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : CKN.localBox (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) Ω' J) (r : ENNReal) : MeasureTheory.MemLp v r (MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω' J))

A field continuous on Q lies in every L^r on a local box of Q.

theorem CIV.component_mem_spaceTimeTestFunction {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hφ : φ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)) (i : Fin 3) : (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ w i) ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)

A component of a vector test function supported in Q is a scalar test function supported in Q.

theorem CIV.integral_pressureGauge_momentum_eq_zero {p p' : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f f' : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hp : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder) (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hp' : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p' z) unitCylinder) (hf' : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f' z) unitCylinder) (hgrad : ∀ z ∈ unitCylinder, ∀ (i : Fin 3), CKN.spatialPartial p' i z - CKN.spatialPartial p i z = f' z i - f z i) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hφ : φ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => (p' z - p z) * ∑ i : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ w i) i z + ∑ i : Fin 3, (f' z i - f z i) * φ z i) MeasureTheory.volume ∧ ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), (p' z - p z) * ∑ i : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ w i) i z + ∑ i : Fin 3, (f' z i - f z i) * φ z i = 0

The momentum pairing of a smooth gauge: if ∇π' - ∇π = f' - f on Q, the pairing ∫ (π' - π) div φ + (f' - f) · φ vanishes for every test field φ supported in Q.

theorem CIV.integral_pressureGauge_energy_eq_zero {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p p' : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f f' : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hp : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder) (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hp' : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p' z) unitCylinder) (hf' : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f' z) unitCylinder) (hdiv : ∀ z ∈ unitCylinder, ∑ j : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) j z = 0) (hgrad : ∀ z ∈ unitCylinder, ∀ (i : Fin 3), CKN.spatialPartial p' i z - CKN.spatialPartial p i z = f' z i - f z i) {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ψ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => (p' z - p z) * ∑ i : Fin 3, u z i * CKN.spatialPartial ψ i z + (∑ i : Fin 3, (f' z i - f z i) * u z i) * ψ z) MeasureTheory.volume ∧ ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), (p' z - p z) * ∑ i : Fin 3, u z i * CKN.spatialPartial ψ i z + (∑ i : Fin 3, (f' z i - f z i) * u z i) * ψ z = 0

The energy pairing of a smooth gauge: if ∇π' - ∇π = f' - f on Q and u is smooth and divergence free there, the pairing ∫ (π' - π) u · ∇ψ + ((f' - f) · u) ψ vanishes for every test function ψ supported in Q.

theorem CIV.isSuitableWeakSolutionIntegrable_of_pressureGauge {q : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p p' : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f f' : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : CKN.IsSuitableWeakSolutionIntegrable (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p f) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hp : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder) (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hp' : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p' z) unitCylinder) (hf' : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f' z) unitCylinder) (hdiv : ∀ z ∈ unitCylinder, ∑ j : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) j z = 0) (hgrad : ∀ z ∈ unitCylinder, ∀ (i : Fin 3), CKN.spatialPartial p' i z - CKN.spatialPartial p i z = f' z i - f z i) : CKN.IsSuitableWeakSolutionIntegrable (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p' f'

Changing the pressure and the force of a suitable weak solution on Q by a smooth gauge: if the velocity, pressure and force are smooth on Q, the velocity is divergence free there, and the smooth fields π', f' satisfy ∇π' - ∇π = f' - f on Q, then (u, π') is a suitable weak solution with the force f'. This is the form of the CKN library class CKN.IsSuitableWeakSolutionIntegrable.

theorem CIV.isSuitableWeakSolution_of_pressureGauge {q : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p p' : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f f' : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p f) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hp : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder) (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hp' : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p' z) unitCylinder) (hf' : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f' z) unitCylinder) (hdiv : ∀ z ∈ unitCylinder, ∑ j : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) j z = 0) (hgrad : ∀ z ∈ unitCylinder, ∀ (i : Fin 3), CKN.spatialPartial p' i z - CKN.spatialPartial p i z = f' z i - f z i) : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p' f'

Changing the pressure and the force of a suitable weak solution on Q by a smooth gauge: if the velocity, pressure and force are smooth on Q, the velocity is divergence free there, and the smooth fields π', f' satisfy ∇π' - ∇π = f' - f on Q, then (u, π') is a suitable weak solution with the force f'.