The mollified transport field

The transport velocity J_ε a of eq:reg-mild-forced is the convolution of a divergence-free L² field with a smooth compactly supported kernel. It is smooth, bounded with bounded first derivatives, and divergence free at every point; these are the hypotheses of the transport cancellation.

noncomputable def CKN.Leray.forcedTransportKernel (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : Foundation.Parabolic.Vec3 → ℝ

The physical form of the regularizing kernel.

Equations

• CKN.Leray.forcedTransportKernel ρ ε hε y = CKN.Leray.regMollifierKernel ρ ε hε (WithLp.toLp 2 y)

theorem CKN.Leray.forcedTransportKernel_contDiff (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : ContDiff ℝ (↑⊤) (forcedTransportKernel ρ ε hε)

theorem CKN.Leray.forcedTransportKernel_hasCompactSupport (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : HasCompactSupport (forcedTransportKernel ρ ε hε)

theorem CKN.Leray.forcedTransport_component_eq {ρ : RegMollifierProfile} {ε : ℝ} (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) (i : Fin 3) : regUniformMollifiedInitial ρ ε hε a x i = MeasureTheory.convolution (forcedTransportKernel ρ ε hε) (fun (y : Foundation.Parabolic.Vec3) => a y i) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

theorem CKN.Leray.forcedTransport_contDiff {ρ : RegMollifierProfile} {ε : ℝ} (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (i : Fin 3) : ContDiff ℝ 1 fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedInitial ρ ε hε a x i

The components of the mollified transport field are smooth.

theorem CKN.Leray.norm_convolution_le_of_memLp_two {κ f : Foundation.Parabolic.Vec3 → ℝ} (hκ : MeasureTheory.MemLp κ 2 MeasureTheory.volume) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) : ‖MeasureTheory.convolution κ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x‖ ≤ (MeasureTheory.eLpNorm κ 2 MeasureTheory.volume * MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal

A scalar convolution of an L² kernel with an L² function is bounded by the product of the norms.

theorem CKN.Leray.forcedTransportKernel_deriv_memLp (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (i : Fin 3) : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => (fderiv ℝ (forcedTransportKernel ρ ε hε) y) (basisVec i)) 2 MeasureTheory.volume

The kernel derivative in a coordinate direction is square integrable.

theorem CKN.Leray.forcedTransport_fderiv_eq {ρ : RegMollifierProfile} {ε : ℝ} (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) (i k : Fin 3) : (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => regUniformMollifiedInitial ρ ε hε a y i) x) (basisVec k) = MeasureTheory.convolution (fun (y : Foundation.Parabolic.Vec3) => (fderiv ℝ (forcedTransportKernel ρ ε hε) y) (basisVec k)) (fun (y : Foundation.Parabolic.Vec3) => a y i) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

The coordinate derivative of a transport component is the convolution with the kernel derivative.

theorem CKN.Leray.forcedTransport_bounded {ρ : RegMollifierProfile} {ε : ℝ} (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : ∃ (M : ℝ), (∀ (x : Foundation.Parabolic.Vec3) (i : Fin 3), ‖regUniformMollifiedInitial ρ ε hε a x i‖ ≤ M) ∧ ∀ (x : Foundation.Parabolic.Vec3) (i : Fin 3), ‖(fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => regUniformMollifiedInitial ρ ε hε a y i) x) (basisVec i)‖ ≤ M

The mollified transport field and its diagonal derivatives are uniformly bounded.

theorem CKN.Leray.forcedTransport_div_eq_zero {ρ : RegMollifierProfile} {ε : ℝ} (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) (x : Foundation.Parabolic.Vec3) : ∑ i : Fin 3, (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => regUniformMollifiedInitial ρ ε hε a y i) x) (basisVec i) = 0

The mollified transport field of a divergence-free field is divergence free at every point.