The transport cancellation for Sobolev velocities

For a smooth bounded divergence-free transport field V with bounded derivatives and a square-integrable velocity u with square-integrable weak gradient, ∑ᵢⱼ ∫ Vᵢ uⱼ ∂ᵢuⱼ = 0. This is the cancellation of the transport term in the energy equality of lem:regularised-forced: for smooth velocities it is an integration by parts of ½ V·∇|u|², and it passes to Sobolev velocities through spatial mollification.

theorem CKN.Leray.integral_mul_fderiv_sq_eq_neg (V w : Foundation.Parabolic.Vec3 → ℝ) (i : Fin 3) (hV : ContDiff ℝ 1 V) (hw : ContDiff ℝ 1 w) (M : ℝ) (hVb : ∀ (x : Foundation.Parabolic.Vec3), ‖V x‖ ≤ M) (hdVb : ∀ (x : Foundation.Parabolic.Vec3), ‖(fderiv ℝ V x) (basisVec i)‖ ≤ M) (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hdw2 : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => (fderiv ℝ w x) (basisVec i)) 2 MeasureTheory.volume) : ∫ (x : Foundation.Parabolic.Vec3), V x * (2 * (w x * (fderiv ℝ w x) (basisVec i))) = -∫ (x : Foundation.Parabolic.Vec3), (fderiv ℝ V x) (basisVec i) * w x ^ 2

Integration by parts of Vᵢ ∂ᵢ(w²) for a smooth square-integrable function with square-integrable derivative and a smooth bounded coefficient with bounded derivative.

theorem CKN.Leray.smooth_transport_cancellation (V w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hV : ∀ (i : Fin 3), ContDiff ℝ 1 fun (x : Foundation.Parabolic.Vec3) => V x i) (hw : ∀ (j : Fin 3), ContDiff ℝ 1 fun (x : Foundation.Parabolic.Vec3) => w x j) (M : ℝ) (hVb : ∀ (x : Foundation.Parabolic.Vec3) (i : Fin 3), ‖V x i‖ ≤ M) (hdVb : ∀ (x : Foundation.Parabolic.Vec3) (i : Fin 3), ‖(fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => V y i) x) (basisVec i)‖ ≤ M) (hdiv : ∀ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => V y i) x) (basisVec i) = 0) (hw2 : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => w x j) 2 MeasureTheory.volume) (hdw2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => w y j) x) (basisVec i)) 2 MeasureTheory.volume) : ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), V x i * (w x j * (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => w y j) x) (basisVec i)) = 0

The transport cancellation for smooth velocities.

theorem CKN.Leray.tendsto_integral_mul_of_tendsto_eLpNorm_two {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (F G : ℕ → α → ℝ) (f g : α → ℝ) (hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) 2 μ) (hG : ∀ (n : ℕ), MeasureTheory.MemLp (G n) 2 μ) (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) (hFc : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - f) 2 μ) Filter.atTop (nhds 0)) (hGc : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (G n - g) 2 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), F n x * G n x ∂μ) Filter.atTop (nhds (∫ (x : α), f x * g x ∂μ))

Products of L²-convergent sequences have convergent integrals.

theorem CKN.Leray.transport_cancellation (V u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3) (hV : ∀ (i : Fin 3), ContDiff ℝ 1 fun (x : Foundation.Parabolic.Vec3) => V x i) (M : ℝ) (hVb : ∀ (x : Foundation.Parabolic.Vec3) (i : Fin 3), ‖V x i‖ ≤ M) (hdVb : ∀ (x : Foundation.Parabolic.Vec3) (i : Fin 3), ‖(fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => V y i) x) (basisVec i)‖ ≤ M) (hdiv : ∀ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => V y i) x) (basisVec i) = 0) (hu2 : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u x j) 2 MeasureTheory.volume) (hD2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => D x i j) 2 MeasureTheory.volume) (hweak : ∀ (i j : Fin 3), HasWeakPartialDerivOn Set.univ i (fun (x : Vec 3) => u x j) fun (x : Vec 3) => D x i j) : ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), V x i * (u x j * D x i j) = 0

The transport cancellation for velocities with square-integrable weak gradients.