Convergence of the commutator of DiPerna and Lions

Step 1 of lem:aniso:comparison is the vanishing, as ε → 0, of the commutator R_ε of eq:aniso:comparison:mollified in L² of every ball. The argument runs in three stages.

For a smooth g the two integrals defining R_ε recombine, after one integration by parts against the kernel and one use of the weak divergence of b, into

R_ε = ∑ᵢ bᵢ (η_ε * ∂ᵢg) - η_ε * (∑ᵢ bᵢ ∂ᵢg),

so that when g is in addition compactly supported both terms are mollifications of continuous compactly supported functions. Each converges uniformly to its own limit and the two limits cancel, the error being controlled by the modulus of continuity of ∇g and of b·∇g at scale ε.

The general case follows from the linearity of R_ε in g together with the L² bound of eq:aniso:comparison:mollified, applied to g - φ with φ a smooth compactly supported approximation of g in L² of the enlarged ball. Such a φ comes from the density of continuous compactly supported functions in L², made smooth by a uniform approximation and returned to compact support by a bump equal to one on the ball.

theorem CIV.abs_integral_mollifierKernel_mul_sub_le {m : ℕ} {ε δ : ℝ} (hε : 0 < ε) {f : CKN.Vec m → ℝ} (hf : Continuous f) (hmod : ∀ (y z : CKN.Vec m), ‖y - z‖ < ε → |f y - f z| ≤ δ) (x : CKN.Vec m) : |(∫ (y : CKN.Vec m), mollifierKernel m ε (x - y) * f y) - f x| ≤ δ

Uniform convergence of the mollification of a continuous function: if f varies by at most δ over distances below ε, then η_ε * f differs from f by at most δ.

Integration by parts against the kernel

The commutator for a smooth function

theorem CIV.diPernaLionsCommutator_eq_of_contDiff {m : ℕ} {ε : ℝ} (hε : 0 < ε) {b : CKN.Vec m → CKN.Vec m} {divb g : CKN.Vec m → ℝ} (hb : Continuous b) (hweak : ∀ (ψ : CKN.Vec m → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (y : CKN.Vec m), divb y * ψ y = -∫ (y : CKN.Vec m), ∑ i : Fin m, b y i * (fderiv ℝ ψ y) (CKN.basisVec i)) (hg : ContDiff ℝ (↑⊤) g) (x : CKN.Vec m) : diPernaLionsCommutator m ε b divb g x = (∑ i : Fin m, b x i * ∫ (y : CKN.Vec m), mollifierKernel m ε (x - y) * (fderiv ℝ g y) (CKN.basisVec i)) - ∫ (y : CKN.Vec m), mollifierKernel m ε (x - y) * ∑ i : Fin m, b y i * (fderiv ℝ g y) (CKN.basisVec i)

For a smooth g the commutator collapses to the difference between the drift applied to the mollified gradient of g and the mollification of the drift applied to that gradient. This is the form of eq:aniso:comparison:mollified in which both terms converge.

The uniform bound on the commutator of a smooth function

Convergence of the commutator of a smooth function

theorem CIV.tendsto_diPernaLionsCommutator_sq_integral_of_contDiff {m : ℕ} {R : ℝ} {Λ : NNReal} {b : CKN.Vec m → CKN.Vec m} {divb g : CKN.Vec m → ℝ} (hlip : LipschitzWith Λ b) (hdivbm : MeasureTheory.AEStronglyMeasurable divb MeasureTheory.volume) (hweak : ∀ (ψ : CKN.Vec m → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (y : CKN.Vec m), divb y * ψ y = -∫ (y : CKN.Vec m), ∑ i : Fin m, b y i * (fderiv ℝ ψ y) (CKN.basisVec i)) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : Filter.Tendsto (fun (ε : ℝ) => ∫ (x : CKN.Vec m) in Metric.closedBall 0 R, diPernaLionsCommutator m ε b divb g x ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Step 1 of lem:aniso:comparison: for a smooth compactly supported g the commutator R_ε of eq:aniso:comparison:mollified tends to zero in L² of every ball.

Linearity of the commutator in the transported function

Approximation by smooth compactly supported functions

theorem CIV.exists_contDiff_hasCompactSupport_integral_sq_sub_le {m : ℕ} {R M : ℝ} {g : CKN.Vec m → ℝ} (hg : ∀ᵐ (y : CKN.Vec m), |g y| ≤ M) (hgm : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) {θ : ℝ} (hθ : 0 < θ) : ∃ (φ : CKN.Vec m → ℝ), ContDiff ℝ (↑⊤) φ ∧ HasCompactSupport φ ∧ ∫ (y : CKN.Vec m) in Metric.closedBall 0 R, (g y - φ y) ^ 2 ≤ θ

Density of smooth compactly supported functions in L² of a ball: a bounded measurable function is approximated there, to any accuracy, by a smooth compactly supported one.

Convergence of the commutator of a bounded measurable function

theorem CIV.tendsto_diPernaLionsCommutator_sq_integral {m : ℕ} {Λ : NNReal} {M R : ℝ} {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) (hweak : ∀ (ψ : CKN.Vec m → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (y : CKN.Vec m), divb y * ψ y = -∫ (y : CKN.Vec m), ∑ i : Fin m, b y i * (fderiv ℝ ψ y) (CKN.basisVec i)) (hg : ∀ᵐ (y : CKN.Vec m), |g y| ≤ M) (hgm : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) : Filter.Tendsto (fun (ε : ℝ) => ∫ (x : CKN.Vec m) in Metric.closedBall 0 R, diPernaLionsCommutator m ε b divb g x ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Step 1 of lem:aniso:comparison: the DiPerna–Lions commutator R_ε of eq:aniso:comparison:mollified converges to zero in L² of every ball as ε → 0, for every bounded measurable g and every Lipschitz drift with bounded weak divergence.