From the weak Navier–Stokes identities to pointwise equations: calculus core

For a field smooth on the open unit cylinder Q and a smooth test function compactly supported in Q, spatial and temporal derivatives move across the integral, and a continuous function on Q whose products with all such test functions integrate to zero vanishes on Q. As a first application the tested divergence identity of a suitable weak solution that is smooth on Q gives div u = 0 pointwise. These are the first steps from the weak formulation to the classical equations used in the proof of lem:aniso:annulus.

theorem CIV.integrable_mul_of_continuousOn_of_tsupport_subset_prod {S : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {g ρ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContinuousOn g S) (hρ : Continuous ρ) (hρc : HasCompactSupport ρ) (hsupp : tsupport ρ ⊆ S) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => g x * ρ x) MeasureTheory.volume

A function continuous on S times a continuous compactly supported function whose support lies in S is integrable on Vec3 × ℝ.

theorem CIV.integral_mul_fderiv_eq_neg_of_contDiffOn {S : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hS : IsOpen S) {h ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hh : ContDiffOn ℝ (↑⊤) h S) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hsupp : tsupport ψ ⊆ S) (v : CKN.Foundation.Parabolic.Vec3 × ℝ) : ∫ (x : CKN.Foundation.Parabolic.Vec3 × ℝ), h x * (fderiv ℝ ψ x) v = -∫ (x : CKN.Foundation.Parabolic.Vec3 × ℝ), (fderiv ℝ h x) v * ψ x

Integration by parts in a direction v of Vec3 × ℝ for a field smooth on an open set S against a test function supported in S.

theorem CIV.integral_mul_spatialPartial_eq_neg_of_contDiffOn {h ψ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hh : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => h z) unitCylinder) (hψ : ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z) (hψc : HasCompactSupport fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z) (hsupp : (tsupport fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z) ⊆ unitCylinder) (i : Fin 3) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), h z * CKN.spatialPartial ψ i z = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.spatialPartial h i z * ψ z

Integration by parts in the spatial direction i on the unit cylinder.

theorem CIV.integral_mul_timePartial_eq_neg_of_contDiffOn {h ψ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hh : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => h z) unitCylinder) (hψ : ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z) (hψc : HasCompactSupport fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z) (hsupp : (tsupport fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z) ⊆ unitCylinder) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), h z * CKN.timePartial ψ z = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.timePartial h z * ψ z

Integration by parts in time on the unit cylinder.

theorem CIV.eq_zero_on_unitCylinder_of_forall_test {F : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hF : ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => F z) unitCylinder) (hzero : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ unitCylinder → ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), F z * ψ z = 0) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ unitCylinder → F z = 0

The fundamental lemma of the calculus of variations on the unit cylinder, pointwise for a continuous function.

theorem CIV.integral_unitCylinder_eq_integral_of_tsupport {F ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hsupp : tsupport ψ ⊆ unitCylinder) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in unitCylinder, F z * ψ z = ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), F z * ψ z

Against a test function supported in the unit cylinder, the integral over the cylinder is the integral over all of space-time.

theorem CIV.spatialPartial_test_eq_fderiv {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialPartial ψ i z = (fderiv ℝ ψ z) (CKN.basisVec i, 0)

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

theorem CIV.timePartial_test_eq_fderiv {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.timePartial ψ z = (fderiv ℝ ψ z) (0, 1)

The time partial of a smooth test function is its joint derivative in the direction (0, 1).

theorem CIV.integrable_mul_spatialPartial_test {h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hh : ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => h z) unitCylinder) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hsupp : tsupport ψ ⊆ unitCylinder) (v : CKN.Foundation.Parabolic.Vec3 × ℝ) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => h z * (fderiv ℝ ψ z) v) MeasureTheory.volume

A function continuous on the unit cylinder times a directional derivative of a test function supported in the cylinder is integrable.

theorem CIV.classical_divergence_free_of_suitable {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) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ unitCylinder → ∑ j : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) j z = 0

A suitable weak solution on the unit cylinder that is smooth there is pointwise divergence free.