Divergence and momentum identities for the viscous shear

theorem CKN.ShearCalculus.integral_restrict_test {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} {U : Set (Foundation.Parabolic.Vec3 × ℝ)} (hsub : tsupport G ⊆ U) (hzero : ∀ z ∉ tsupport G, F z = 0) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in U, F z = ∫ (z : Foundation.Parabolic.Vec3 × ℝ), F z

Restriction does not change an integral supported on a test support.

theorem CKN.ShearCalculus.spatial_zero {G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hG : ContDiff ℝ (↑⊤) G) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport G) (i : Fin 3) : spatialPartial G i z = 0

A spatial test derivative vanishes off the support of the test.

theorem CKN.ShearCalculus.time_zero {G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hG : ContDiff ℝ (↑⊤) G) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport G) : timePartial G z = 0

A time test derivative vanishes off the support of the test.

theorem CKN.ShearCalculus.coordinate_support (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (i : Fin 3) : (tsupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => φ z i) ⊆ tsupport φ

A coordinate of a vector test has support contained in the vector support.

theorem CKN.shearFlow_divergence (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (hψ : ψ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 1)) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, shearFlow z i * spatialPartial ψ i z) (tsupport ψ) MeasureTheory.volume ∧ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 1), ∑ i : Fin 3, shearFlow z i * spatialPartial ψ i z = 0

The incompressibility test identity, including its integrability clause.

theorem CKN.shearFlow_momentum (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 1)) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => -∑ i : Fin 3, shearFlow z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, shearFlow z i * shearFlow z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, shearFlowGrad z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z) (tsupport φ) MeasureTheory.volume ∧ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 1), -∑ i : Fin 3, shearFlow z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, shearFlow z i * shearFlow z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, shearFlowGrad z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z = 0

The momentum test identity with zero pressure and zero force.