The weak gradient of a suitable weak solution pairs as the distributional gradient

For a suitable weak solution on the unit cylinder, the weak gradient Du satisfies ∫ Du_{kj} ∂ⱼψ = -∫ u_k ∂ⱼ∂ⱼψ for every smooth test function ψ supported in the cylinder. The proof works on a local box containing the support of ψ, applies the weak derivative on almost every time slice, and integrates in time. This identifies the viscous term of the weak momentum equation in the passage to the classical equations used in the proof of lem:aniso:annulus.

theorem CIV.continuous_vec3EuclideanNorm_fst : Continuous fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Foundation.Parabolic.vec3EuclideanNorm z.1

theorem CIV.exists_localBox_of_isCompact_subset_unitCylinder {K : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hK : IsCompact K) (hKQ : K ⊆ unitCylinder) : ∃ (r : ℝ) (a : ℝ) (b : ℝ), 0 < r ∧ r < 1 ∧ -1 < a ∧ a < b ∧ b < 0 ∧ K ⊆ CKN.Foundation.Parabolic.vec3Ball 0 r ×ˢ Set.Ioo a b

A compact subset of the unit cylinder lies in a local box B(0, r) × (a, b).

theorem CIV.localBox_ball_Ioo {r a b : ℝ} (hr : 0 < r) (hr1 : r < 1) (ha : -1 < a) (hb : b < 0) : CKN.localBox (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) (CKN.Foundation.Parabolic.vec3Ball 0 r) (Set.Ioo a b)

The box B(0, r) × (a, b) with r < 1 and -1 < a < b < 0 is a local box of the unit cylinder.

theorem CIV.spatialPartial_eq_zero_of_eventually_eq_zero {F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hF : ∀ᶠ (w : CKN.Foundation.Parabolic.Vec3 × ℝ) in nhds z, F w = 0) (j : Fin 3) : CKN.spatialPartial F j z = 0

A spatial partial vanishes where the function vanishes on a neighbourhood.

theorem CIV.contDiff_spatialPartial_of_contDiff {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (j : Fin 3) : ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial ψ j z

The spatial partial of a smooth function is its joint derivative in the direction (eⱼ, 0), hence smooth.

theorem CIV.integrable_and_integral_weakGradient_mul_spatialPartial {q : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {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) {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hsupp : tsupport ψ ⊆ unitCylinder) (k j : Fin 3) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Du z k j * CKN.spatialPartial ψ j z) MeasureTheory.volume ∧ ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), Du z k j * CKN.spatialPartial ψ j z = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), u z k * CKN.spatialSecondPartial ψ j j z

For a suitable weak solution on the unit cylinder, the weak gradient pairs with a test function supported in the cylinder as the distributional gradient.

theorem CIV.integral_weakGradient_mul_spatialPartial_eq {q : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {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) {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hsupp : tsupport ψ ⊆ unitCylinder) (k j : Fin 3) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), Du z k j * CKN.spatialPartial ψ j z = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), u z k * CKN.spatialSecondPartial ψ j j z

For a suitable weak solution on the unit cylinder, the weak gradient pairs with a test function supported in the cylinder as the distributional gradient.