Weak-derivative identities for the regularized convolution

The convolution associated with eq:reg-mollifier commutes with scalar weak spatial derivatives. Its vector-valued divergence constraint is preserved.

theorem CKN.Leray.smoothCompactConvolution_spatialDeriv_eq_of_weak {κ f g : Foundation.Parabolic.Vec3 → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hκc : HasCompactSupport κ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) (j : Fin 3) (hweak : HasWeakPartialDerivOn Set.univ j f g) (x : Foundation.Parabolic.Vec3) : MeasureTheory.ConvolutionExists κ g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume ∧ spatialDeriv (MeasureTheory.convolution κ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) j x = MeasureTheory.convolution κ g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

A smooth compactly supported convolution kernel commutes with a scalar weak partial derivative on all of space.

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

The scalar kernel on the Euclidean coordinate carrier associated with regMollifierKernel.

Equations

• CKN.Leray.regUniformMollifierKernel ρ ε hε x = CKN.Leray.regMollifierKernel ρ ε hε (WithLp.toLp 2 x)

def CKN.Leray.regUniformMollifierCoordinateTuple (n : ℕ) (w : Fin n → Fin 3) : Fin n → Foundation.Parabolic.Vec3

The tuple of coordinate directions associated with an ordered derivative.

Equations

• CKN.Leray.regUniformMollifierCoordinateTuple n w k = CKN.basisVec (w k)

theorem CKN.Leray.regMollifyVector_iteratedDerivative_enorm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (n : ℕ) (v : Fin n → Foundation.Parabolic.L2Vec3) (x : Foundation.Parabolic.L2Vec3) : ‖(iteratedFDeriv ℝ n (regMollifyVector ρ ε hε f) x) v‖ₑ ≤ MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.L2Vec3) => (iteratedFDeriv ℝ n (regMollifierKernel ρ ε hε) y) v) 2 MeasureTheory.volume * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

Every ordered derivative of vector mollification is bounded by the corresponding derivative-kernel norm times the input's L² norm.

theorem CKN.Leray.regMollifierLemmaAssembly_bounds (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (n : ℕ) (v : Fin n → Foundation.Parabolic.L2Vec3) (x : Foundation.Parabolic.L2Vec3) : MeasureTheory.eLpNorm (regMollifyVector ρ ε hε f) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm f 2 MeasureTheory.volume ∧ ‖(iteratedFDeriv ℝ n (regMollifyVector ρ ε hε f) x) v‖ₑ ≤ ENNReal.ofReal (ε ^ (-(3 / 2) - ↑n)) * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.L2Vec3) => (iteratedFDeriv ℝ n (⇑ρ.rho) y) v) 2 MeasureTheory.volume * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

The all-orders smoothing estimate and spatial L² contraction for the regularizing operator.

theorem CKN.Leray.regUniformMollifiedInitial_coordinateDerivative_bound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (n : ℕ) (w : Fin n → Fin 3) (i : Fin 3) (x : Foundation.Parabolic.Vec3) : ‖(iteratedFDeriv ℝ n (fun (y : Foundation.Parabolic.Vec3) => regUniformMollifiedInitial ρ ε hε a y i) x) (regUniformMollifierCoordinateTuple n w)‖ₑ ≤ MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => (iteratedFDeriv ℝ n (regUniformMollifierKernel ρ ε hε) y) (regUniformMollifierCoordinateTuple n w)) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => a y i) 2 MeasureTheory.volume

Every ordered coordinate derivative of a mollified component is bounded pointwise by the L² norm of the corresponding differentiated kernel times the L² norm of the input component.

theorem CKN.Leray.regUniformMollifiedInitial_spatialDeriv_eq_weak (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (g : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (hg : ∀ (i j : Fin 3), MeasureTheory.LocallyIntegrable (g i j) MeasureTheory.volume) (hweak : ∀ (i j : Fin 3), HasWeakPartialDerivOn Set.univ j (fun (x : Vec 3) => a x i) (g i j)) (x : Foundation.Parabolic.Vec3) (i j : Fin 3) : spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => regUniformMollifiedInitial ρ ε hε a y i) j x = MeasureTheory.convolution (regUniformMollifierKernel ρ ε hε) (g i j) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

Classical derivatives of the mollified vector field equal the mollified function-valued weak derivatives coordinate by coordinate.

theorem CKN.Leray.regMollifierLemmaAssembly_preserves_divergence (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsWeakDivFreeL2 a) : IsWeakDivFreeL2 (regUniformMollifiedInitial ρ ε hε a)

The regularized initial field remains in the Leray space; in particular, its weak divergence is zero.