Countable generation of sub-σ-algebras modulo null sets (R4 converse piece 3, #107)

The generic, signature-free toolkit behind the coherent factor realization: a sub-σ-algebra of a separable measure space is generated, modulo null sets, by a countable family of events, and a countable family of events yields an honest factor map to a Cantor-type space.

Nothing here mentions relational structures; the whole file is a Mathlib-upstream candidate (tracked on #24).

Design note: what "modulo null sets" means

The mod-null statement is deliberately eventwise:

∀ E, MeasurableSet[m] E → ∃ E', MeasurableSet[generateFrom G] E' ∧ E' =ᵐ[μ] E

and not an equality of measurable spaces "modulo null sets". A σ-algebra-level formulation would force a choice between Measure.trim and Measure.completion at every use site and generate diamonds between them; the eventwise form composes without any such commitment, and it is exactly what the factor recursion consumes.

Contents

• MeasureTheory.Measure.MeasureDense.exists_generateFrom_ae_eq_of_ne_top — the upgrade from approximation to a.e. representatives: if G is measure-dense for the trimmed measure, every m-measurable event of finite trimmed measure agrees a.e. with a generateFrom G-measurable one. Proved by summable symmetric-difference approximation and Borel–Cantelli — measure density alone gives only approximation, which is not the consumer API. No countability of G is required; countability matters only when G is turned into a factor space. exists_generateFrom_ae_eq is the [IsFiniteMeasure μ] corollary.
• MeasureTheory.measure_symmDiff_threshold_le — the threshold estimate ν (E ∆ {x | 1/2 < f x}) ≤ 2 * ‖1_E - f‖₁, which converts an L¹-dense family of functions into a measure-dense family of sets. This is the bridge from separability of Lᵖ to separability of the measure.
• MeasureTheory.isSeparable_trim — separability descends to a sub-σ-algebra: IsSeparable μ → IsSeparable (μ.trim hm). This is the theorem the coherent factor realization rests on and it is not in Mathlib. Stated as a theorem rather than an instance: with both m and m0 in scope an instance invites measurable-space instance drift at every use site.
• MeasureTheory.exists_measurable_comap_ae_generates — factor existence for one sub-σ-algebra: over a separable finite measure, m ≤ m0 admits an m-measurable Cantor-space factor map whose pullback sits inside m and captures every m-event modulo null sets. This is the single-algebra statement only — see its docstring for why it does not extend to a coherent family.
• MeasurableSpace.comap_mapNatBool — the missing companion to Mathlib's measurable_mapNatBool: a countably generated σ-algebra is literally the pullback of the Cantor-space σ-algebra along mapNatBool, with no SeparatesPoints hypothesis, since injectivity of the factor map is irrelevant to the pullback identity.

The Cantor factor of a countably generated σ-algebra

theorem MeasurableSpace.comap_mapNatBool (X : Type u_1) [m : MeasurableSpace X] [CountablyGenerated X] : MeasurableSpace.comap (mapNatBool X) inferInstance = m

The Cantor factor is exact: a countably generated σ-algebra is literally the pullback of the Cantor-space σ-algebra along MeasurableSpace.mapNatBool — no null sets involved. This is the missing companion to Mathlib's measurable_mapNatBool / injective_mapNatBool: it needs CountablyGenerated but not SeparatesPoints, since injectivity of the factor map is irrelevant to the pullback identity.

Monotonicity of measure density

theorem MeasureTheory.Measure.MeasureDense.mono {Y : Type u_2} [MeasurableSpace Y] {ν : Measure Y} {𝒜 ℬ : Set (Set Y)} (h𝒜 : ν.MeasureDense 𝒜) (hsub : 𝒜 ⊆ ℬ) (hmeas : ∀ s ∈ ℬ, MeasurableSet s) : ν.MeasureDense ℬ

A larger family of measurable sets is still measure-dense. Not in Mathlib, and needed whenever a dense family is enlarged — e.g. when a chosen family is embedded into a bigger indexed one. Both hypotheses are necessary: the inclusion gives the approximation, and measurability of the larger family is not implied by it.

From approximation to a.e. representatives

theorem MeasureTheory.Measure.MeasureDense.exists_generateFrom_ae_eq_of_ne_top {X : Type u_1} {m0 : MeasurableSpace X} {μ : Measure X} {m : MeasurableSpace X} (hm : m ≤ m0) {G : Set (Set X)} (hG : (μ.trim hm).MeasureDense G) {E : Set X} (hE : MeasurableSet E) (hμE : (μ.trim hm) E ≠ ⊤) : ∃ (E' : Set X), MeasurableSet E' ∧ E' =ᵐ[μ] E

Measure density upgrades to a.e. representatives. If G is measure-dense for the trimmed measure μ.trim hm, then every m-measurable event of finite trimmed measure has a generateFrom G-measurable a.e. representative.

This is the statement the factor construction consumes: measure density by itself provides only approximation, whereas the recursion needs actual representatives. The gap is closed by choosing approximants with summable errors and applying Borel–Cantelli — the representative is limsup t n, and E ∆ limsup t n is contained in the limsup of the error sets.

No countability of G is needed here; countability matters only when G is turned into a factor space.

theorem MeasureTheory.Measure.MeasureDense.exists_generateFrom_ae_eq {X : Type u_1} {m0 : MeasurableSpace X} {μ : Measure X} {m : MeasurableSpace X} (hm : m ≤ m0) [IsFiniteMeasure μ] {G : Set (Set X)} (hG : (μ.trim hm).MeasureDense G) {E : Set X} (hE : MeasurableSet E) : ∃ (E' : Set X), MeasurableSet E' ∧ E' =ᵐ[μ] E

Measure density upgrades to a.e. representatives, finite-measure form — the shape the R4 factor construction uses, where the ambient measure is a probability measure and the finiteness side condition is automatic.

The threshold estimate

theorem MeasureTheory.measure_symmDiff_threshold_le {X : Type u_1} {m : MeasurableSpace X} (ν : Measure X) {E : Set X} {f : X → ℝ} (hE : MeasurableSet E) (hf : AEStronglyMeasurable f ν) : ν (symmDiff E {x : X | 1 / 2 < f x}) ≤ 2 * eLpNorm ((E.indicator fun (x : X) => 1) - f) 1 ν

The threshold estimate: thresholding an L¹ function at 1/2 produces a set whose symmetric difference with E is controlled by the L¹ distance to the indicator of E,

ν (E ∆ {x | 1/2 < f x}) ≤ 2 * ‖1_E - f‖₁.

This is what converts an L¹-dense family of functions into a measure-dense family of sets, and hence the separability of Lᵖ into the separability of the measure. The proof is Markov's inequality applied to 1_E - f, which has norm at least 1/2 on the symmetric difference: where E holds but the threshold fails the difference is at least 1 - 1/2, and where the threshold holds but E fails it exceeds 1/2.

Separability descends to a sub-σ-algebra

theorem MeasureTheory.isSeparable_trim {X : Type u_1} {m0 : MeasurableSpace X} {μ : Measure X} {m : MeasurableSpace X} (hm : m ≤ m0) [IsSeparable μ] : IsSeparable (μ.trim hm)

Separability descends to Measure.trim. If μ is separable on the ambient σ-algebra m0, the trimmed measure is separable on any sub-σ-algebra m ≤ m0.

This is the theorem the coherent factor realization rests on, and it is not in Mathlib. The route is: Lp ℝ 1 μ is second-countable because μ is separable; the subgroup lpMeasSubgroup ℝ m 1 μ of m-measurable classes inherits second countability as a subtype; lpMeasSubgroupToLpTrimIso transports it to Lp ℝ 1 (μ.trim hm); a countable dense family there is thresholded at 1/2 into a countable family of m-measurable sets, and measure_symmDiff_threshold_le turns L¹ density of the functions into measure density of the sets.

Exposed as a theorem rather than an instance: with both m and m0 in scope, an instance would be a standing invitation to measurable-space instance drift at every use site.

The factor map of a single sub-σ-algebra

theorem MeasureTheory.exists_measurable_comap_ae_generates {X : Type u_1} {m0 : MeasurableSpace X} {μ : Measure X} {m : MeasurableSpace X} (hm : m ≤ m0) [IsSeparable μ] [IsFiniteMeasure μ] : ∃ (q : X → ℕ → Bool), Measurable q ∧ ∀ (E : Set X), MeasurableSet E → ∃ (E' : Set X), MeasurableSet E' ∧ E' =ᵐ[μ] E

Factor existence for one sub-σ-algebra: over a separable finite measure, any sub-σ-algebra m ≤ m0 admits a Cantor-space factor map q such that

• q is m-measurable — equivalently comap q ≤ m, via Measurable.comap_le, so only the measurability is stated; and
• every m-event agrees a.e. with a comap q-event.

So comap q captures m exactly modulo null sets, while remaining an honest pullback — the statement never asserts an equality of σ-algebras "modulo null sets".

This assembles the three preceding results: isSeparable_trim produces a countable measure-dense family for the trimmed measure, that family generates a countably generated sub-σ-algebra whose Cantor factor is exact by comap_mapNatBool, and Measure.MeasureDense.exists_generateFrom_ae_eq supplies the a.e. representatives.

This is the single-algebra statement only. It is deliberately not the tool for a coherent family: mapNatBool is built from a typeclass-chosen generating sequence, which provides neither literal index inclusion for C ⊆ A nor equivariance between different members of a family. A coherent family needs a common index set chosen up front.