The kernel majorizing both terms of the commutator together

theorem CIV.cauchy_schwarz_kernel {m : ℕ} {K g : CKN.Vec m → ℝ} (hK_nonneg : ∀ (y : CKN.Vec m), 0 ≤ K y) (hK_int : MeasureTheory.Integrable K MeasureTheory.volume) (hKg_int : MeasureTheory.Integrable (fun (y : CKN.Vec m) => K y * |g y|) MeasureTheory.volume) (hKg2_int : MeasureTheory.Integrable (fun (y : CKN.Vec m) => K y * g y ^ 2) MeasureTheory.volume) : (∫ (y : CKN.Vec m), K y * |g y|) ^ 2 ≤ (∫ (y : CKN.Vec m), K y) * ∫ (y : CKN.Vec m), K y * g y ^ 2

Cauchy-Schwarz for the integral of a nonnegative kernel against |g| and against g^2: (∫ K |g|)^2 ≤ (∫ K) (∫ K g^2). This is the elementary inequality behind the L² bound on eq:aniso:comparison:mollified, applied pointwise to the kernel majorizing the commutator.

noncomputable def CIV.commutatorMajorant (m : ℕ) (ε Λ : ℝ) : CKN.Vec m → ℝ

The nonnegative kernel Λ (ε ∑ᵢ|∂ᵢη_ε| + η_ε) majorizing, jointly, both integrands of diPernaLionsCommutator. It has the same total mass Λ (C_η + 1) as the uniform bound of eq:aniso:comparison:mollified, and it vanishes outside the ball of radius ε.

Equations

• CIV.commutatorMajorant m ε Λ w = Λ * (ε * ∑ i : Fin m, |(fderiv ℝ (CIV.mollifierKernel m ε) w) (CKN.basisVec i)| + CIV.mollifierKernel m ε w)

theorem CIV.commutatorMajorant_nonneg {m : ℕ} {ε Λ : ℝ} (hε : 0 < ε) (hΛ : 0 ≤ Λ) (w : CKN.Vec m) : 0 ≤ commutatorMajorant m ε Λ w

theorem CIV.commutatorMajorant_eq_zero {m : ℕ} {ε Λ : ℝ} (hε : 0 < ε) {w : CKN.Vec m} (hw : ε < ‖w‖) : commutatorMajorant m ε Λ w = 0

theorem CIV.continuous_commutatorMajorant {m : ℕ} (ε Λ : ℝ) : Continuous (commutatorMajorant m ε Λ)

theorem CIV.hasCompactSupport_commutatorMajorant {m : ℕ} {ε : ℝ} (hε : 0 < ε) (Λ : ℝ) : HasCompactSupport (commutatorMajorant m ε Λ)

theorem CIV.integrable_commutatorMajorant {m : ℕ} {ε : ℝ} (hε : 0 < ε) (Λ : ℝ) : MeasureTheory.Integrable (commutatorMajorant m ε Λ) MeasureTheory.volume

theorem CIV.integral_commutatorMajorant {m : ℕ} {ε : ℝ} (hε : 0 < ε) (Λ : ℝ) : ∫ (w : CKN.Vec m), commutatorMajorant m ε Λ w = Λ * (mollifierGradConst m + 1)

The total mass of the majorant is Λ (C_η + 1), matching the uniform bound abs_diPernaLionsCommutator_le.

theorem CIV.integral_commutatorMajorant_sub {m : ℕ} {ε : ℝ} (hε : 0 < ε) (Λ : ℝ) (x : CKN.Vec m) : ∫ (y : CKN.Vec m), commutatorMajorant m ε Λ (x - y) = Λ * (mollifierGradConst m + 1)

theorem CIV.integral_commutatorMajorant_sub' {m : ℕ} {ε : ℝ} (hε : 0 < ε) (Λ : ℝ) (y : CKN.Vec m) : ∫ (x : CKN.Vec m), commutatorMajorant m ε Λ (x - y) = Λ * (mollifierGradConst m + 1)

theorem CIV.exists_bound_commutatorMajorant {m : ℕ} {ε : ℝ} (hε : 0 < ε) (Λ : ℝ) : ∃ (C0 : ℝ), ∀ (w : CKN.Vec m), commutatorMajorant m ε Λ w ≤ C0

The majorant kernel is globally bounded: being continuous with compact support, it attains a finite maximum over all of Vec m.

The pointwise domination of the commutator by the majorant kernel

theorem CIV.abs_diPernaLionsCommutator_le_kernel {m : ℕ} {ε M : ℝ} {Λ : NNReal} (hε : 0 < ε) {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| ≤ ∫ (y : CKN.Vec m), commutatorMajorant m ε (↑Λ) (x - y) * |g y|

The commutator is dominated, pointwise in x, by the majorant kernel against |g|: |R_ε(x)| ≤ ∫ y, commutatorMajorant (x - y) |g(y)| dy. This keeps the factor g y explicit (rather than replacing it by the uniform bound M, as abs_diPernaLionsCommutator_le does), which is what the L² estimate on eq:aniso:comparison:mollified needs.

Measurability of the commutator as a function of x

theorem CIV.aestronglyMeasurable_diPernaLionsCommutator {m : ℕ} (ε : ℝ) {b : CKN.Vec m → CKN.Vec m} {divb g : CKN.Vec m → ℝ} (hb : Continuous b) (hdivbm : MeasureTheory.AEStronglyMeasurable divb MeasureTheory.volume) (hgm : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) : MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Vec m) => diPernaLionsCommutator m ε b divb g x) MeasureTheory.volume

The commutator x ↦ R_ε(x) is a.e. strongly measurable: each defining integral is the x-marginal of a jointly measurable integrand on Vec m × Vec m.

The L² bound on a ball

theorem CIV.integral_sq_diPernaLionsCommutator_le {m : ℕ} {ε R 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) in Metric.closedBall 0 R, diPernaLionsCommutator m ε b divb g x ^ 2 ≤ (↑Λ * (mollifierGradConst m + 1)) ^ 2 * ∫ (y : CKN.Vec m) in Metric.closedBall 0 (R + ε), g y ^ 2

The L² bound on a ball for the DiPerna–Lions commutator of eq:aniso:comparison:mollified: the commutator on closedBall 0 R is controlled by g on the slightly larger closedBall 0 (R + ε), with a constant depending only on m, Λ, and the fixed profile's gradient constant mollifierGradConst m.