Mollified fluxes at a fixed time

At a fixed time the tested momentum flux of a mollified component is rewritten with the weak product rule, the weak-gradient transport through mollification and integrations by parts in the mollification variable. The result expresses the cross-testing integrand of lem:pv-serrin-uniqueness through mollified velocities, gradients, convection terms and pressures.

theorem ESS.serrin_mollify_spatialDeriv {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) {ε : ℝ} (hε : 0 < ε) (j : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) : CKN.spatialDeriv (CKN.mollify f ε hε) j y = ∫ (x : CKN.Foundation.Parabolic.Vec3), f x * CKN.spatialDeriv (CKN.mollifier ε hε) j (y - x)

The spatial derivative of a mollification is the integral against the differentiated kernel.

theorem ESS.serrin_mollify_of_ae_zero {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : f =ᵐ[MeasureTheory.volume] 0) {ε : ℝ} (hε : 0 < ε) (y : CKN.Foundation.Parabolic.Vec3) : CKN.mollify f ε hε y = 0

The mollification of an almost everywhere vanishing function vanishes.

theorem ESS.serrin_slice_convection {w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hDw2 : MeasureTheory.MemLp Dw 2 MeasureTheory.volume) (hgrad : ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => w x i) fun (x : CKN.Vec 3) => Dw x i) (htr : ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, Dw x j j = 0) {ρ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hρ : ContDiff ℝ (↑⊤) ρ) (hρc : HasCompactSupport ρ) (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) : ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), w x k * w x j * CKN.spatialDeriv ρ j (y - x) = ∫ (x : CKN.Foundation.Parabolic.Vec3), (∑ j : Fin 3, w x j * Dw x k j) * ρ (y - x)

The convection part of a tested flux, rewritten with the weak product rule and the divergence condition.

theorem ESS.serrin_slice_flux_integral (n : ℕ) {w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pw : CKN.Foundation.Parabolic.Vec3 → ℝ} (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hDw2 : MeasureTheory.MemLp Dw 2 MeasureTheory.volume) (hgrad : ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => w x i) fun (x : CKN.Vec 3) => Dw x i) (htr : ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, Dw x j j = 0) (hpw : MeasureTheory.LocallyIntegrable pw MeasureTheory.volume) (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) : ∫ (x : CKN.Foundation.Parabolic.Vec3), -∑ j : Fin 3, w x k * w x j * CKN.spatialDeriv (serrinKernel n) j (y - x) + ∑ j : Fin 3, Dw x k j * CKN.spatialDeriv (serrinKernel n) j (y - x) - pw x * CKN.spatialDeriv (serrinKernel n) k (y - x) = -CKN.mollify (fun (x : CKN.Vec 3) => ∑ j : Fin 3, w x j * Dw x k j) (serrinRadius n) ⋯ y + ∑ j : Fin 3, CKN.spatialDeriv (CKN.mollify (fun (x : CKN.Vec 3) => Dw x k j) (serrinRadius n) ⋯) j y - CKN.spatialDeriv (CKN.mollify pw (serrinRadius n) ⋯) k y

The tested flux of a mollified component, integrated in the mollification point: convection, diffusion and pressure contributions.

theorem ESS.serrin_slice_flux_pairing (n : ℕ) {w z : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Dw Dz : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pw : CKN.Foundation.Parabolic.Vec3 → ℝ} (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hDw2 : MeasureTheory.MemLp Dw 2 MeasureTheory.volume) (hwgrad : ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => w x i) fun (x : CKN.Vec 3) => Dw x i) (hwtr : ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, Dw x j j = 0) (hpw : MeasureTheory.LocallyIntegrable pw MeasureTheory.volume) (hz2 : MeasureTheory.MemLp z 2 MeasureTheory.volume) (hDz2 : MeasureTheory.MemLp Dz 2 MeasureTheory.volume) (hzgrad : ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => z x i) fun (x : CKN.Vec 3) => Dz x i) (hztr : ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, Dz x j j = 0) {η : CKN.Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) : ∫ (y : CKN.Foundation.Parabolic.Vec3), η y * ∑ k : Fin 3, (∫ (x : CKN.Foundation.Parabolic.Vec3), -∑ j : Fin 3, w x k * w x j * CKN.spatialDeriv (serrinKernel n) j (y - x) + ∑ j : Fin 3, Dw x k j * CKN.spatialDeriv (serrinKernel n) j (y - x) - pw x * CKN.spatialDeriv (serrinKernel n) k (y - x)) * ∫ (x : CKN.Foundation.Parabolic.Vec3), z x k * serrinKernel n (y - x) = ∫ (y : CKN.Foundation.Parabolic.Vec3), -(η y * ∑ k : Fin 3, CKN.mollify (fun (x : CKN.Vec 3) => z x k) (serrinRadius n) ⋯ y * CKN.mollify (fun (x : CKN.Vec 3) => ∑ j : Fin 3, w x j * Dw x k j) (serrinRadius n) ⋯ y) - η y * ∑ k : Fin 3, ∑ j : Fin 3, CKN.mollify (fun (x : CKN.Vec 3) => Dz x k j) (serrinRadius n) ⋯ y * CKN.mollify (fun (x : CKN.Vec 3) => Dw x k j) (serrinRadius n) ⋯ y - ∑ k : Fin 3, ∑ j : Fin 3, CKN.spatialDeriv η j y * CKN.mollify (fun (x : CKN.Vec 3) => z x k) (serrinRadius n) ⋯ y * CKN.mollify (fun (x : CKN.Vec 3) => Dw x k j) (serrinRadius n) ⋯ y + ∑ k : Fin 3, CKN.spatialDeriv η k y * CKN.mollify (fun (x : CKN.Vec 3) => z x k) (serrinRadius n) ⋯ y * CKN.mollify pw (serrinRadius n) ⋯ y

The cutoff-weighted pairing of the tested fluxes of one field with the mollified components of another, at a fixed time, in integrated-by-parts form.