The x-uniformity crossing: joint measurability of the comparison identity

Representative.mollifySlice_ae_ae_sub_eq_intervalIntegral proves, for each fixed spatial point x, that the mollified slice's change between two times τ₁, τ₂ equals the interval integral of the right side of eq:aniso:comparison:mollified, for a.e. τ₁, τ₂ ∈ I. The exceptional null set of bad (τ₁, τ₂) pairs may depend on x. The next stage of the comparison argument (spatial integration of this identity) instead needs the identity to hold, for one fixed pair (τ₁, τ₂) (or a.e. one), for a.e. x simultaneously — a statement about the product measure on Vec m × I × I, strictly stronger than "for every x, the x-slice is null".

This file closes that crossing. The route: restate the bad set purely in terms of the two honest, everywhere-defined functions mollifySlice and the right side of the mollified equation; show both are jointly AEStronglyMeasurable in (x, τ); apply the abstract crossing lemma ae_prod_prod_eq_of_forall_ae_ae (a two-layer Fubini/Tonelli argument through the measurable representatives of each side) to upgrade "for every x, a.e. (τ₁, τ₂)" to "jointly a.e. (x, τ₁, τ₂)"; then swap the product order (as in SliceBounds.IsLocallyBoundedOn.ae_slice_bound) to read it off as "a.e. (τ₁, τ₂), a.e. x", the shape the spatial integration needs.

Contents

• A countable compact exhaustion of an open subset of ℝ (exists_compact_exhaustion_of_isOpen), built from compactCovering of the open set as a topological subspace.
• A single x-independent "good time set" G ⊆ I of full measure, assembled from the exhaustion, on which the per-τ hypotheses IsLocallyBoundedOn only supplies for a.e. τ on each compact hold for every τ ∈ G (exists_good_time_set).
• Joint measurability, in (x, τ), of mollifySlice, of partialLaplacian/gradPair applied to mollifySlice, and hence of the whole right side of eq:aniso:comparison:mollified (aestronglyMeasurable_comparisonRHS) — the joint measurability of the DiPerna–Lions commutator term is ComparisonLimits.aestronglyMeasurable_diPernaLionsCommutator_prod.
• Joint measurability of the parametrized interval integral (x, τ₁, τ₂) ↦ ∫ s in τ₁..τ₂, f x s.
• The abstract two-layer crossing lemma ae_prod_prod_eq_of_forall_ae_ae, and its application to close the crossing (mollifySlice_ae_prod_sub_eq_intervalIntegral).

Part 0: a countable compact exhaustion of an open subset of ℝ

theorem CIV.exists_compact_exhaustion_of_isOpen {I : Set ℝ} (hI : IsOpen I) : ∃ (J : ℕ → Set ℝ), (∀ (n : ℕ), IsCompact (J n)) ∧ Monotone J ∧ (∀ (n : ℕ), J n ⊆ I) ∧ ⋃ (n : ℕ), J n = I

Every open subset of ℝ is the increasing union of a countable family of compact subsets. Built from the canonical compact exhaustion (compactCovering) of the open set regarded as a topological subspace: an open subset of a locally compact, second-countable space is itself locally compact and (hence) σ-compact.

Part 1: the x-independent good time set

theorem CIV.exists_good_time_set {m : ℕ} {I : Set ℝ} (hI : IsOpen I) {q : CKN.Vec m × ℝ → ℝ} (hq : IsLocallyBoundedOn m I q) : ∃ G ⊆ I, MeasureTheory.volume (I \ G) = 0 ∧ ∀ τ ∈ G, MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Vec m) => q (x, τ)) MeasureTheory.volume ∧ ∃ (M : ℝ), ∀ᵐ (x : CKN.Vec m), |q (x, τ)| ≤ M

A single time set G ⊆ I, of full measure in I and independent of any spatial point, on which the per-τ hypotheses IsLocallyBoundedOn supplies only for a.e. τ on each compact J ⊆ I hold for every τ ∈ G: q(·, τ) is AEStronglyMeasurable and bounded a.e. Assembled from a compact exhaustion J n ↗ I (exists_compact_exhaustion_of_isOpen) plus the countable union of the per-J n exceptional null sets.

Part 2: joint measurability of the individual right-side terms

theorem CIV.aestronglyMeasurable_mollifySlice {m : ℕ} {ε : ℝ} {q : CKN.Vec m × ℝ → ℝ} {μs : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μs] (hqmeas : MeasureTheory.AEStronglyMeasurable q (MeasureTheory.volume.prod μs)) : MeasureTheory.AEStronglyMeasurable (fun (p : CKN.Vec m × ℝ) => mollifySlice m ε q p) (MeasureTheory.volume.prod μs)

Piece 1. Joint AEStronglyMeasurableness, in (x, τ), of the spatial mollification mollifySlice. Since mollifySlice_apply is the unconditional closed formula mollifySlice m ε q (x, τ) = ∫ y, mollifierKernel m ε (x - y) * q (y, τ), this follows directly from aestronglyMeasurable_kernelIntegral; no side hypothesis on q beyond joint measurability is needed.

theorem CIV.aestronglyMeasurable_partialLaplacianKernelIntegral {m : ℕ} {ε : ℝ} (d : ℕ) {q : CKN.Vec m × ℝ → ℝ} {μs : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μs] (hqmeas : MeasureTheory.AEStronglyMeasurable q (MeasureTheory.volume.prod μs)) : MeasureTheory.AEStronglyMeasurable (fun (p : CKN.Vec m × ℝ) => ∫ (y : CKN.Vec m), partialLaplacianKernel m d ε (p.1 - y) * q (y, p.2)) (MeasureTheory.volume.prod μs)

Joint measurability of the kernel formula for partialLaplacian (mollifySlice ...), again a direct instance of aestronglyMeasurable_kernelIntegral.

theorem CIV.aestronglyMeasurable_gradPairKernelIntegral {m : ℕ} {ε : ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {q : CKN.Vec m × ℝ → ℝ} {μs : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μs] (hBmeas : Measurable B) (hqmeas : MeasureTheory.AEStronglyMeasurable q (MeasureTheory.volume.prod μs)) : MeasureTheory.AEStronglyMeasurable (fun (p : CKN.Vec m × ℝ) => ∫ (y : CKN.Vec m), (fderiv ℝ (mollifierKernel m ε) (p.1 - y)) (B p) * q (y, p.2)) (MeasureTheory.volume.prod μs)

Joint measurability of the kernel formula for gradPair (mollifySlice ...) B: unlike the plain kernel integral, the direction B p fed to fderiv also varies jointly with (x, τ), so the argument first expands the directional derivative in the coordinate basis (sum_smul_basisVec) to isolate B's dependence from the kernel's.

theorem CIV.aestronglyMeasurable_partialLaplacian_mollifySlice {m : ℕ} {ε : ℝ} (hε : 0 < ε) (d : ℕ) {I : Set ℝ} (hI : IsOpen I) {q : CKN.Vec m × ℝ → ℝ} (hq : IsLocallyBoundedOn m I q) : MeasureTheory.AEStronglyMeasurable (fun (p : CKN.Vec m × ℝ) => partialLaplacian m d (mollifySlice m ε q) p) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict I))

Piece 3, part a. partialLaplacian m d (mollifySlice m ε q) is jointly AEStronglyMeasurable in (x, τ) ∈ Vec m × I. The kernel formula partialLaplacian_mollifySlice holds pointwise on Vec m × G (the good time set of exists_good_time_set), where it agrees with the everywhere jointly measurable aestronglyMeasurable_partialLaplacianKernelIntegral; the complement Vec m × (I \ G) is null in the product measure since volume (I \ G) = 0.

theorem CIV.aestronglyMeasurable_gradPair_mollifySlice {m : ℕ} {ε : ℝ} (hε : 0 < ε) {I : Set ℝ} (hI : IsOpen I) {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (hq : IsLocallyBoundedOn m I q) : MeasureTheory.AEStronglyMeasurable (fun (p : CKN.Vec m × ℝ) => gradPair m (mollifySlice m ε q) p (B p)) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict I))

Piece 3, part b. fun p => gradPair m (mollifySlice m ε q) p (B p) is jointly AEStronglyMeasurable in (x, τ) ∈ Vec m × I, by the same good-time-set congruence argument as aestronglyMeasurable_partialLaplacian_mollifySlice, using gradPair_mollifySlice's kernel formula in place of partialLaplacian_mollifySlice's.

theorem CIV.aestronglyMeasurable_comparisonRHS {m d : ℕ} {ε : ℝ} (hε : 0 < ε) {I : Set ℝ} (hI : IsOpen I) {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (hq : IsLocallyBoundedOn m I q) : MeasureTheory.AEStronglyMeasurable (fun (p : CKN.Vec m × ℝ) => partialLaplacian m d (mollifySlice m ε q) p - gradPair m (mollifySlice m ε q) p (B p) + 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 (MeasureTheory.volume.restrict I))

Piece 3, assembled. The whole right side of eq:aniso:comparison:mollified is jointly AEStronglyMeasurable in (x, τ) ∈ Vec m × I: the sum of the three terms just shown measurable (aestronglyMeasurable_partialLaplacian_mollifySlice, aestronglyMeasurable_gradPair_mollifySlice) plus the DiPerna–Lions commutator term, whose joint measurability is ComparisonLimits.aestronglyMeasurable_diPernaLionsCommutator_prod.

Part 3: joint measurability of the parametrized interval integral

theorem CIV.aestronglyMeasurable_intervalIntegral {m : ℕ} {f : CKN.Vec m → ℝ → ℝ} {μx : MeasureTheory.Measure (CKN.Vec m)} {μτ : MeasureTheory.Measure (ℝ × ℝ)} {μI : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μI] (hf : MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Vec m × ℝ) => f z.1 z.2) (μx.prod μI)) : MeasureTheory.AEStronglyMeasurable (fun (p : CKN.Vec m × ℝ × ℝ) => ∫ (s : ℝ) in p.2.1..p.2.2, f p.1 s ∂μI) (μx.prod μτ)

Piece 4. Joint measurability of the parametrized interval integral (x, τ₁, τ₂) ↦ ∫ s in τ₁..τ₂, f x s ∂μI, from joint measurability of f in (x, s) alone. Unfolds the interval integral as the difference of two one-sided set integrals (aestronglyMeasurable_setIntegral_Ioc, applied with the two endpoint roles swapped) and uses that intervalIntegral is definitionally exactly that difference.

Part 4: the abstract crossing

theorem CIV.ae_prod_prod_eq_of_forall_ae_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ν1 ν2 : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite ν1] [MeasureTheory.SFinite ν2] {f g : α × ℝ × ℝ → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (μ.prod (ν1.prod ν2))) (hg : MeasureTheory.AEStronglyMeasurable g (μ.prod (ν1.prod ν2))) (h : ∀ (a : α), ∀ᵐ (b1 : ℝ) ∂ν1, ∀ᵐ (b2 : ℝ) ∂ν2, f (a, b1, b2) = g (a, b1, b2)) : f =ᵐ[μ.prod (ν1.prod ν2)] g

The abstract crossing at the heart of the comparison chain's structural blocker. Given two functions on a triple product, jointly AEStronglyMeasurable, that agree for every point a of the first factor at a.e. point (b₁, b₂) of the other two, they agree at a.e. point of the whole product jointly. The exceptional a.e. set in the hypothesis may depend on a; the conclusion's does not privilege any factor.

The proof passes to the measurable representatives F', G' of f, g (AEStronglyMeasurable.mk). Since F', G' are measurable everywhere (not just a.e.), every one of their a-slices is genuinely measurable with no exceptional set, so the hypothesis's nested a.e. statement (available for a.e. a, where f, g agree with F', G' slice-wise) upgrades to a product statement on that slice via Measure.ae_prod_iff_ae_ae — the two-variable Fubini/Tonelli fact that does need measurability. Chaining f =ᵐ F', F' =ᵐ G', G' =ᵐ g slice-wise gives f =ᵐ g for a.e. a, and one more application of the same Fubini/Tonelli fact (now on the full product) closes it.

Part 5: the crossing, applied

theorem CIV.mollifySlice_ae_prod_sub_eq_intervalIntegral {m d : ℕ} {I : Set ℝ} (hI : IsOpen I) (hIoc : I.OrdConnected) {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (hq : IsLocallyBoundedOn m I q) (heq : IsDistributionalDriftDiffusion m d I B divB q) {ε : ℝ} (hε : 0 < ε) {τ₀ : ℝ} (hτ₀ : τ₀ ∈ I) : ∀ᵐ (τ1 : ℝ) (τ2 : ℝ) ∂MeasureTheory.volume.restrict I, ∀ᵐ (x : CKN.Vec m), mollifySlice m ε q (x, τ2) - mollifySlice m ε q (x, τ1) = ∫ (s : ℝ) in τ1..τ2, partialLaplacian m d (mollifySlice m ε q) (x, s) - gradPair m (mollifySlice m ε q) (x, s) (B (x, s)) + diPernaLionsCommutator m ε (fun (y : CKN.Vec m) => B (y, s)) (fun (y : CKN.Vec m) => divB (y, s)) (fun (y : CKN.Vec m) => q (y, s)) x

The structural blocker, fully closed. For a.e. (τ₁, τ₂) ∈ I × I and a.e. x, the mollified slice's change between τ₁ and τ₂ equals the interval integral of the right side of eq:aniso:comparison:mollified — upgrading Representative.mollifySlice_ae_ae_sub_eq_intervalIntegral (true for every x, a.e. τ₁, τ₂, with the exceptional set possibly depending on x) to hold jointly a.e., the form spatial integration of the identity needs.

The proof restates the bad set purely from the two honest, everywhere-defined sides of the identity, shows both jointly AEStronglyMeasurable in (x, τ₁, τ₂) (aestronglyMeasurable_mollifySlice, aestronglyMeasurable_comparisonRHS composed with aestronglyMeasurable_intervalIntegral), and applies the abstract crossing ae_prod_prod_eq_of_forall_ae_ae followed by a Prod.swap pushforward (as in SliceBounds.IsLocallyBoundedOn.ae_slice_bound) to read the conclusion in the (τ₁, τ₂)-first order.