Spatial integration by parts for the regularized pairing derivative

At a fixed positive time, the regularized momentum equation paired with a smooth, compactly supported, divergence-free field reduces to the viscous term with both derivatives on the test and the transport term with one derivative on the test. This is the spatial computation in the proof of lem:reg-equicontinuity.

theorem CKN.Leray.lerayHopfLimit_integrable_mul_compact {f g : Foundation.Parabolic.Vec3 → ℝ} (hf : Continuous f) (hg : Continuous g) (hgc : HasCompactSupport g) : MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => f x * g x) MeasureTheory.volume

A continuous scalar field times a continuous compactly supported field is integrable.

theorem CKN.Leray.lerayHopfLimit_pairing_equation_ibp (f : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (g : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (h : Fin 3 → Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (P : Foundation.Parabolic.Vec3 → ℝ) (q J F w : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (hf : ∀ (i : Fin 3), Continuous (f i)) (hfdiff : ∀ (i : Fin 3) (x : Foundation.Parabolic.Vec3), DifferentiableAt ℝ (f i) x) (hfd : ∀ (i j : Fin 3) (x : Foundation.Parabolic.Vec3), (fderiv ℝ (f i) x) (basisVec j) = g i j x) (hg : ∀ (i j : Fin 3), Continuous (g i j)) (hgdiff : ∀ (i j : Fin 3) (x : Foundation.Parabolic.Vec3), DifferentiableAt ℝ (g i j) x) (hgd : ∀ (i j k : Fin 3) (x : Foundation.Parabolic.Vec3), (fderiv ℝ (g i j) x) (basisVec k) = h i j k x) (hh : ∀ (i j k : Fin 3), Continuous (h i j k)) (hP : Continuous P) (hPdiff : ∀ (x : Foundation.Parabolic.Vec3), DifferentiableAt ℝ P x) (hPd : ∀ (i : Fin 3) (x : Foundation.Parabolic.Vec3), (fderiv ℝ P x) (basisVec i) = q i x) (hq : ∀ (i : Fin 3), Continuous (q i)) (hJ : ∀ (j : Fin 3), ContDiff ℝ 1 (J j)) (hdivJ : ∀ (x : Foundation.Parabolic.Vec3), ∑ j : Fin 3, (fderiv ℝ (J j) x) (basisVec j) = 0) (hF : ∀ (i : Fin 3) (x : Foundation.Parabolic.Vec3), F i x = ∑ j : Fin 3, h i j j x - ∑ j : Fin 3, J j x * g i j x - q i x) (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hwc : ∀ (i : Fin 3), HasCompactSupport (w i)) (hdivw : ∀ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, spatialDeriv (w i) i x = 0) : ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, F i x * w i x = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (f i x * spatialDeriv (spatialDeriv (w i) j) j x + f i x * J j x * spatialDeriv (w i) j x)

Pairing the classical regularized momentum equation at one time with a smooth compactly supported divergence-free field. Here f i is the velocity component, g i j its j-th partial derivative, h i j k the partial derivative of g i j, P the pressure with partials q, and J the divergence-free transport velocity.