Fixed-time convection identities for H² fields

At a fixed time the convection field (u·∇)u of a solenoidal H² field is square integrable, and pairing it with a smooth compactly supported field integrates by parts onto the transported product u ⊗ u (lem:lps-H1-estimate).

theorem ESS.lps_h1_convection_term_memLp_two {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2u : CKN.Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hu2 : MeasureTheory.MemLp u 2 MeasureTheory.volume) (hDu2 : MeasureTheory.MemLp Du 2 MeasureTheory.volume) (hD2u2 : MeasureTheory.MemLp D2u 2 MeasureTheory.volume) (hH1 : ∀ (i : Fin 3), ∃ (h : CKN.H1Function Set.univ), (h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) => Du x i j) (hgrad : ∀ (i j : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => Du x i j) fun (x : CKN.Vec 3) => D2u x i j) (j k : Fin 3) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u x j * Du x k j) 2 MeasureTheory.volume

Each term uⱼ ∂ⱼuₖ of the convection field of an H² field is square integrable: the velocity is in L⁶ and the gradient in L³ by Sobolev interpolation (lem:lps-H1-estimate).

theorem ESS.lps_h1_convection_memLp_two {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2u : CKN.Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hu2 : MeasureTheory.MemLp u 2 MeasureTheory.volume) (hDu2 : MeasureTheory.MemLp Du 2 MeasureTheory.volume) (hD2u2 : MeasureTheory.MemLp D2u 2 MeasureTheory.volume) (hH1 : ∀ (i : Fin 3), ∃ (h : CKN.H1Function Set.univ), (h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) => Du x i j) (hgrad : ∀ (i j : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => Du x i j) fun (x : CKN.Vec 3) => D2u x i j) (k : Fin 3) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, u x j * Du x k j) 2 MeasureTheory.volume

The convection field (u·∇)u of a solenoidal H² field is square integrable (lem:lps-H1-estimate).

theorem ESS.lps_h1_convection_test_identity {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2u : CKN.Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hu2 : MeasureTheory.MemLp u 2 MeasureTheory.volume) (hDu2 : MeasureTheory.MemLp Du 2 MeasureTheory.volume) (hD2u2 : MeasureTheory.MemLp D2u 2 MeasureTheory.volume) (hH1 : ∀ (i : Fin 3), ∃ (h : CKN.H1Function Set.univ), (h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) => Du x i j) (hgu : ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => u x i) fun (x : CKN.Vec 3) => Du x i) (hgrad : ∀ (i j : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => Du x i j) fun (x : CKN.Vec 3) => D2u x i j) (htr : ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, Du x j j = 0) (hψ : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => ψ x i) (hψc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => ψ x i) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, u x i * u x j * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y i) j x = -∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (∑ j : Fin 3, u x j * Du x i j) * ψ x i

Pairing the convection field with a smooth compactly supported field integrates by parts onto the transported product u ⊗ u, since u is solenoidal (lem:lps-H1-estimate).

theorem ESS.lps_h1_laplacian_test_identity {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2u : CKN.Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hgrad : ∀ (i j : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => Du x i j) fun (x : CKN.Vec 3) => D2u x i j) (hψ : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => ψ x i) (hψc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => ψ x i) (hDu2 : MeasureTheory.MemLp Du 2 MeasureTheory.volume) (hD2u2 : MeasureTheory.MemLp D2u 2 MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du x i j * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y i) j x = -∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (∑ j : Fin 3, D2u x i j j) * ψ x i

Pairing the second-derivative trace with a smooth compactly supported field integrates by parts onto the first derivatives (lem:lps-H1-estimate).

theorem ESS.lps_h1_laplacian_weak_div_free {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2u : CKN.Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hu2 : MeasureTheory.MemLp u 2 MeasureTheory.volume) (hDu2 : MeasureTheory.MemLp Du 2 MeasureTheory.volume) (hD2u2 : MeasureTheory.MemLp D2u 2 MeasureTheory.volume) (hgu : ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => u x i) fun (x : CKN.Vec 3) => Du x i) (hgrad : ∀ (i j : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => Du x i j) fun (x : CKN.Vec 3) => D2u x i j) (hdiv : ∀ (ψ : CKN.WeakTestFunction Set.univ), ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u x i * ψ.partialDeriv i x = 0) : CKN.IsWeakDivFreeL2 fun (x : CKN.Foundation.Parabolic.Vec3) (i : Fin 3) => ∑ j : Fin 3, D2u x i j j

The second-derivative trace of a weakly solenoidal H² field is weakly solenoidal (lem:lps-H1-estimate).