The commutator of DiPerna and Lions

Mollifying eq:aniso:comparison:equation in space produces the commutator R_ε = B·∇(η_ε * q) - η_ε * (B·∇q) of eq:aniso:comparison:mollified. Since B·∇q means div(Bq) - (div B) q, the convolution η_ε * (B·∇q) is the integral of q against the derivative of the kernel, and the commutator is the explicit integral

R_ε(x) = ∫ q(y) (b(x) - b(y))·(∇η_ε)(x - y) dy + ∫ η_ε(x - y) (div b)(y) q(y) dy,

taken here as its definition for one time slice b = B(·, τ), q = q(·, τ).

The estimate below is the uniform bound of eq:aniso:comparison:mollified: the first integrand is supported where |x - y| ≤ ε, where the Lipschitz bound on b gains the factor ε that cancels the 1/ε of the gradient of the kernel. The constant is explicit, Λ M_∞ (C_η + 1) with C_η the gradient constant of the profile.

noncomputable def CIV.diPernaLionsCommutator (m : ℕ) (ε : ℝ) (b : CKN.Vec m → CKN.Vec m) (divb g : CKN.Vec m → ℝ) (x : CKN.Vec m) : ℝ

The commutator R_ε of eq:aniso:comparison:mollified for one time slice, written as an explicit integral against the kernel η_ε and its gradient.

Equations

• One or more equations did not get rendered due to their size.

theorem CIV.abs_diPernaLionsCommutator_le {m : ℕ} {ε M : ℝ} {Λ : NNReal} (hε : 0 < ε) (hM : 0 ≤ M) {b : CKN.Vec m → CKN.Vec m} {divb g : CKN.Vec m → ℝ} (hlip : LipschitzWith Λ b) (hdivb : ∀ (y : CKN.Vec m), |divb y| ≤ ↑Λ) (hdivbm : MeasureTheory.AEStronglyMeasurable divb MeasureTheory.volume) (hg : ∀ (y : CKN.Vec m), |g y| ≤ M) (hgm : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (x : CKN.Vec m) : |diPernaLionsCommutator m ε b divb g x| ≤ ↑Λ * M * (mollifierGradConst m + 1)

The uniform bound |R_ε| ≤ C(m, η) Λ M_∞ of eq:aniso:comparison:mollified.