StepSevenAeMerge

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The countable-L almost-everywhere merge

The gap this module closes

flagged, for the future hstep4 supplier, that the proved §4.3 producers put the infrared-cutoff quantifier OUTSIDE the almost-everywhere quantifier. For instance the excess-decay lane's harmonic-approximation provider concludes

  ∀ L m n : ℤ, m ≤ L → … → ∀ᵐ ω ∂(law M), P L m n ω ,

whereas the §4.4 consumer needs the SINGLE null set

  ∀ᵐ ω ∂(law M), ∀ L : ℤ, m ≤ L → P L m n ω .

The exchange is legitimate because ℤ is countable, and it is exactly Mathlib's MeasureTheory.ae_all_iff / MeasureTheory.ae_ball_iff. The merge is proved here as a standalone measure-theoretic lemma: this module imports only Mathlib, in particular no §4.3 file, so no §4.3 statement is touched or re-elaborated.

What is provided

• ae_forall_of_forall_ae_of_countable — the plain countable-index exchange with a guard predicate: from ∀ i, Q i → ∀ᵐ a, P i a conclude ∀ᵐ a, ∀ i, Q i → P i a. The guard Q is arbitrary; the guarded index need not range over a subtype.

No measurability hypothesis appears anywhere: the a.e. filter is a CountableInterFilter, and the merge uses nothing else.

References

• Mathlib, MeasureTheory.ae_all_iff, MeasureTheory.ae_ball_iff.
• The excess-decay seal-distance lane (the consumer whose quantifier order motivates this file; NOT imported).

1. The guarded countable exchange

theorem Algsuperdiff.Section4.Provider.Regularity.ae_forall_of_forall_ae_of_countable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Sort u_2} [Countable ι] {Q : ι → Prop} {P : ι → α → Prop} (h : ∀ (i : ι), Q i → ∀ᵐ (a : α) ∂μ, P i a) : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), Q i → P i a

The countable a.e. merge, with a guard.

  (∀ i, Q i → ∀ᵐ a ∂μ, P i a)   ⟹   ∀ᵐ a ∂μ, ∀ i, Q i → P i a .

The guarded indices form a countable subfamily of a countable family, so the exceptional set is a countable union of null sets. No measurability of P is needed.