The local energy identity for the viscous shear

Two spatial integrations by parts and one time integration by parts give the energy identity, hence the local energy inequality for nonnegative tests.

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

The energy identity holds for every compactly supported smooth scalar test.