Analytic infrastructure for the ε ↓ 0 limit of lem:aniso:comparison

This module supplies the two analytic limits used in step 5b of the comparison lemma, where the mollification parameter ε is sent to zero in the energy E of CIV.Comparison.EnergyInequality.

The spatial mollifier η_ε of CIV.Comparison.Mollifier has unit mass, so convolving a bounded measurable function against it does not increase the squared L² mass on a ball, up to enlarging the ball by ε; this is the quantitative form of the classical fact that an approximate identity contracts on L² (integral_sq_mollifierKernel_convolution_le). Combined with the uniform convergence of the mollification of a smooth compactly supported approximant (from CIV.Comparison.CommutatorConvergence), this gives the L²-of-every-ball convergence of the spatial mollification of a bounded a.e.-measurable time slice to that slice as ε → 0 (tendsto_integral_sq_mollifySlice_sub).

The second limit concerns the DiPerna–Lions commutator. Its squared L² mass on a ball, commutatorL2Sq, is a.e. strongly measurable in the time slice (aestronglyMeasurable_commutatorL2Sq), and its time integral over a compact interval vanishes as ε ↓ 0 (tendsto_integral_commutatorL2Sq), by dominated convergence from the per-slice vanishing of CIV.Comparison.CommutatorConvergence.

The comparison proof uses both limits to pass to ε ↓ 0 in the integrated energy inequality (CIV.ae_ae_le_barrier_of_referenceTime).

The mollifier is an L² contraction

L² convergence of the spatial mollification

L² convergence of mollifySlice

theorem CIV.tendsto_integral_sq_mollifySlice_sub {m : ℕ} {M R τ : ℝ} {q : CKN.Vec m × ℝ → ℝ} (hqb : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ M) (hqm : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) : Filter.Tendsto (fun (ε : ℝ) => ∫ (x : CKN.Vec m) in Metric.closedBall 0 R, (mollifySlice m ε q (x, τ) - q (x, τ)) ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Step 5b's core analytic fact: the spatial mollification of a bounded a.e.-measurable time slice converges to it in L² of every ball as ε → 0.

Vanishing of the commutator, integrated over a compact time interval

noncomputable def CIV.commutatorL2Sq (m : ℕ) (ε Rb : ℝ) (B : CKN.Vec m × ℝ → CKN.Vec m) (divB q : CKN.Vec m × ℝ → ℝ) (s : ℝ) : ℝ

The squared L² mass on a ball of the DiPerna–Lions commutator of one time slice.

Equations

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

Joint measurability of the commutator's ball mass in the time slice

theorem CIV.aestronglyMeasurable_diPernaLionsCommutator_prod {m : ℕ} {ε : ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} {μs : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μs] (hBmeas : Measurable B) (hdivBmeas : Measurable divB) (hqmeas : MeasureTheory.AEStronglyMeasurable q (MeasureTheory.volume.prod μs)) : MeasureTheory.AEStronglyMeasurable (fun (p : CKN.Vec m × ℝ) => diPernaLionsCommutator m ε (fun (y : CKN.Vec m) => B (y, p.2)) (fun (y : CKN.Vec m) => divB (y, p.2)) (fun (y : CKN.Vec m) => q (y, p.2)) p.1) (MeasureTheory.volume.prod μs)

Joint AEStronglyMeasurableness, in the pair (x, s) : Vec m × ℝ, of the DiPerna–Lions commutator transported along a time-parametrized drift B, its divergence, and a time-parametrized function q: from B and its divergence jointly measurable in space-time and q jointly AEStronglyMeasurable on Vec m × ℝ against (volume : Measure (Vec m)).prod μs for any SFinite measure μs on the time axis, the commutator itself — built at each fixed time slice s from the space-time restrictions of B, its divergence, and q, and evaluated at the spatial point x — is jointly AEStronglyMeasurable against the product measure. This is the three-variable extension of aestronglyMeasurable_diPernaLionsCommutator's two-variable argument: it bundles (x, s) into one product factor and integrates the spatial variable y of the commutator's two defining integrals out of it. It is the shared step behind aestronglyMeasurable_commutatorL2Sq, which squares and ball-restricts this fact before integrating x out entirely.

theorem CIV.aestronglyMeasurable_commutatorL2Sq {m : ℕ} {ε Rb τ₀ tplus : ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} (hBmeas : Measurable B) (hdivBmeas : Measurable divB) (hqmeas : MeasureTheory.AEStronglyMeasurable q (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioc τ₀ tplus))) : MeasureTheory.AEStronglyMeasurable (fun (s : ℝ) => commutatorL2Sq m ε Rb B divB q s) (MeasureTheory.volume.restrict (Set.Ioc τ₀ tplus))

Joint measurability of the DiPerna–Lions commutator's squared L² mass on a ball in the time slice s: given B and its divergence jointly measurable in space-time and q a.e. strongly measurable on ℝ^m × (τ₀, τ₊], the ball integral commutatorL2Sq is a.e. strongly measurable as a function of s alone. This reduces to aestronglyMeasurable_diPernaLionsCommutator_prod for the joint (x, s)-measurability of the commutator itself, then repeats a y-integration a second time to remove x itself, over the ball, threading the ball restriction through an indicator since AEStronglyMeasurable.integral_prod_right' integrates over the whole space.

The integrated vanishing of the commutator as ε ↓ 0

theorem CIV.tendsto_integral_commutatorL2Sq {m : ℕ} {I : Set ℝ} {Rb τ₀ tplus : ℝ} (hτ : τ₀ ≤ tplus) {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (hq : IsLocallyBoundedOn m I q) (hsub : Set.Icc τ₀ tplus ⊆ I) : Filter.Tendsto (fun (ε : ℝ) => ∫ (s : ℝ) in τ₀..tplus, commutatorL2Sq m ε Rb B divB q s) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Step 5b's remaining analytic core: for an admissible drift and a locally bounded transported function on a common domain I ⊇ [τ₀, τ₊], the commutator's squared L² mass, time-integrated over (τ₀, τ₊], vanishes as ε ↓ 0. This combines the joint measurability just proved with the per-slice ε → 0 vanishing tendsto_diPernaLionsCommutator_sq_integral and the per-slice L² domination integral_sq_diPernaLionsCommutator_le via dominated convergence along the countably-generated filter 𝓝[>] 0 (MeasureTheory.tendsto_integral_filter_of_dominated_convergence).