Commit 2026-08-15 14:21 97b6a17d

refactor(UniformIntegrable): change the definition of UnifIntegrable (#42092) From ∀ ⦃ε : ℝ⦄ (_ : 0 < ε), ∃ (δ : ℝ) (_ : 0 < δ), ∀ i s, MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε to Tendsto (fun ε ↦ ⨆ (i : ι) (s : Set α) (_ : μ s ≤ ε), eLpNorm (f i) p (μ.restrict s)) (𝓝 0) (𝓝 0) Mains effects are first to work directly in ℝ≥0∞ instead of working in ℝ or ℝ≥0 and coercing, with tends to simplify everything but needs extensive fixes, and secondly to benefit from all the library developed for filters. Another suggestion was to use the definition Tendsto (fun s ↦ ⨆ (i : ι), eLpNorm (f i) p (μ.restrict s)) (comap μ (𝓝 0)) (𝓝 0), which is cleaner, but hard to use due to the lack of lemmas around (comap μ (𝓝 0)). This might be interesting in the future if this latter filter see some other use, but is somewhat cumbersome right now. For now, lemmas unifIntegrable_iff and unifIntegrable_iff' provide the equivalence between the new and the old definitions (modulo the coercion), which is useful to limit the modifications of downstream results. I intend to keep working on this file to put lemmas and proofs more directly in line with the newer definition. For reference, Zulip thread about this PR and the end goal: #mathlib4 > MeasureTheory: Refactoring UniformIntegrable