feat(Integral/Lebesgue): Uniform integrability for ENNReal-valued functions

[D-Thomine]

A version of Mathlib.MeasureTheory.Function.UniformIntegrable for ENNReal-valued function. Needed for a project in dynamics (Kac's lemma). I may also rewrite Mathlib.MeasureTheory.Function.UniformIntegrable to use this file as a foundation.

---

[github-actions]

PR summary 3b9982e671

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.Integral.Lebesgue.UniformIntegrable (new file)	1588

---

Declarations diff (regex)

+ NeZero.top
+ UnifLIntegrable
+ UnifLIntegrable.add
+ UnifLIntegrable.mono_ae
+ UnifLIntegrable.restrict
+ UnifLIntegrable.tendsto_comp_set
+ UnifLIntegrable.uniformLIntegrable
+ UniformLIntegrable
+ UniformLIntegrable.add
+ UniformLIntegrable.lintegral_lt_top_of_isFinite
+ UniformLIntegrable.mono_ae
+ UniformLIntegrable.restrict
+ UniformLIntegrable.unifLIntegrable
+ UniformLIntegrable.uniformTail
+ UniformTail
+ UniformTail.add
+ UniformTail.mono_ae
+ UniformTail.restrict
+ _root_.Finite.uniformLIntegrable
+ iInf_mul_le_setLIntegral₀
+ setLIntegral_le_add_lintegral
+ setLIntegral_le_iSup_mul₀
+ tendsto_iSup_setLIntegral_zero
+ tendsto_measure_preimage_zero
+ tendsto_setLIntegral_preimage_zero
+ unifLIntegrable_congr_ae
+ unifLIntegrable_const
+ unifLIntegrable_def
+ unifLIntegrable_empty
+ unifLIntegrable_mk
+ unifLIntegrable_of_finite
+ uniforLIntegrable_congr_ae
+ uniformLIntegrable_const
+ uniformLIntegrable_def
+ uniformLIntegrable_empty
+ uniformLIntegrable_iff_unifLIntegrable_uniformTail
+ uniformTail_congr_ae
+ uniformTail_const
+ uniformTail_def
+ uniformTail_empty
+ uniformTail_of_finite
+ uniformTail_of_lintegral_lt_top

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 3b9982e).

• +41 new declarations
• −0 removed declarations

+ENNReal.NeZero.top
+Finite.uniformLIntegrable
+MeasureTheory.UnifLIntegrable
+MeasureTheory.UnifLIntegrable.add
+MeasureTheory.UnifLIntegrable.mono_ae
+MeasureTheory.UnifLIntegrable.restrict
+MeasureTheory.UnifLIntegrable.tendsto_comp_set
+MeasureTheory.UnifLIntegrable.uniformLIntegrable
+MeasureTheory.UniformLIntegrable
+MeasureTheory.UniformLIntegrable.add
+MeasureTheory.UniformLIntegrable.lintegral_lt_top_of_isFinite
+MeasureTheory.UniformLIntegrable.mono_ae
+MeasureTheory.UniformLIntegrable.restrict
+MeasureTheory.UniformLIntegrable.unifLIntegrable
+MeasureTheory.UniformLIntegrable.uniformTail
+MeasureTheory.UniformTail
+MeasureTheory.UniformTail.add
+MeasureTheory.UniformTail.mono_ae
+MeasureTheory.UniformTail.restrict
+MeasureTheory.iInf_mul_le_setLIntegral₀
+MeasureTheory.setLIntegral_le_iSup_mul₀
+MeasureTheory.tendsto_iSup_setLIntegral_zero
+MeasureTheory.tendsto_measure_preimage_zero
+MeasureTheory.tendsto_setLIntegral_preimage_zero
+MeasureTheory.unifLIntegrable_congr_ae
+MeasureTheory.unifLIntegrable_const
+MeasureTheory.unifLIntegrable_def
+MeasureTheory.unifLIntegrable_empty
+MeasureTheory.unifLIntegrable_mk
+MeasureTheory.unifLIntegrable_of_finite
+MeasureTheory.uniforLIntegrable_congr_ae
+MeasureTheory.uniformLIntegrable_const
+MeasureTheory.uniformLIntegrable_def
+MeasureTheory.uniformLIntegrable_empty
+MeasureTheory.uniformLIntegrable_iff_unifLIntegrable_uniformTail
+MeasureTheory.uniformTail_congr_ae
+MeasureTheory.uniformTail_const
+MeasureTheory.uniformTail_def
+MeasureTheory.uniformTail_empty
+MeasureTheory.uniformTail_of_finite
+MeasureTheory.uniformTail_of_lintegral_lt_top

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 3b9982e671
Reference commit 2c973492e6

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[CoolRmal]

This doesn't feel like the right approach. Note that UnifIntegrable is defined by using MeasureTheory.eLpNorm, which only requires ENorm. My suggestions would be:

1. Replace the assumption [NormedAddCommGroup β] in the definition of UnifIntegrable and UniformIntegrable with [TopologicalSpace β] [ENorm β] (I am not sure whether [ENorm β] is enough, and if it is not enough then maybe consider using ESeminormedAddMonoid or its variants, and I'll leave it to you to figure this out).
2. After you changed the definition, examine other lemmas in UniformIntegrable.lean, check which theorems still require [NormedAddCommGroup β] (e.g. I think theorems like UnifIntegrable.neg and UnifIntegrable.sub still requires [NormedAddCommGroup β]).
3. Maybe reorganize the file according to the assumptions used (e.g. one section contains lemmas that use [ESeminormedAddMonoid β], and another section contains lemmas that use [NormedAddCommGroup β]).

[CoolRmal]

awaiting-author

[D-Thomine]

I see your point, and I agree that it is what we would like to have in the end.

That said, I wish it were that simple. The current file Function.UnifIntegrable is a thousand lines long and an absolute mess in terms of coercions, maladapted or too strong hypotheses... To give an idea: proving that a single Lp function is UnifIntegrable (MemLp.eLpNorm_indicator_le) takes some 200 lines and uses the NNNorm defined on Lp, which uses itself the [NormedAddCommGroup β] instance (even if the end result doesn't)... Most lemmas and proofs would have to be extensively rewritten.

My motivation was both to have results directly written for ENNReal-valued functions (without needed a simplification step), and to decouple the Enorms and the integral manipulations in Function.UnifIntegrable. Basically write

UnifIntegrable f p μ ↔ UnifLIntegrable (fun i x ↦ ‖f i x‖ₑ ^ p) μ

and delete half of the proofs/auxiliary lemmas in Function.UnifIntegrable. That's probably faster than trying to fix it, and it'll also add some flexibility the day you need something a bit exotic like the uniform integrability of e.g. |f| ln |f|.

[CoolRmal]

If you think it is overly hard then maybe you can open a Zulip thread to discuss this.

Basically write UnifIntegrable f p μ ↔ UnifLIntegrable (fun i x ↦ ‖f i x‖ₑ ^ p) μ

Well I think we should never have sth like this. We should pursue sth like UnifIntegrable f p μ ↔ UnifIntegrable (fun i x ↦ ‖f i x‖ₑ ^ p) μ, similar to MeasureTheory.integrable_enorm_iff.