feat: integral of EReal-valued functions

[gaetanserre]

Duplicate of #41239 for better editing.

Co-authored-by: Rémy Degenne remy.degenne@inria.fr

---

• depends on: [Merged by Bors] - feat: lemmas about operations on EReal #41246
• depends on: [Merged by Bors] - chore: generalize instPosPart to SubNegMonoid #41247
• depends on: feat: variants of Measurable.oneLePart and related lemmas #41322

[github-actions]

PR summary e9f5d5d2b3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.Integral.EReal.AuxLemmas (new file)	1534
Mathlib.MeasureTheory.Integral.EReal.EIntegrable (new file)	1585
Mathlib.MeasureTheory.Integral.EReal.EIntegral (new file)	1602
Mathlib.MeasureTheory.Integral.EReal.Kernel (new file)	1707
Mathlib.MeasureTheory.Integral.EReal.Bochner (new file)	2307
Mathlib.MeasureTheory.Integral.EReal.Prod (new file)	2394

---

Declarations diff (regex)

+ AEMeasurable.leOnePart'
+ AEMeasurable.oneLePart'
+ EIntegrable
+ EIntegrable.add_const
+ EIntegrable.add_real_const
+ EIntegrable.const_add
+ EIntegrable.const_mul
+ EIntegrable.const_sub
+ EIntegrable.eintegral_posPartFun_ne_top_or_eintegral_negPartFun_ne_top
+ EIntegrable.neg
+ EIntegrable.nnreal_smul_measure
+ EIntegrable.real_const_add
+ EIntegrable.real_const_mul
+ EIntegrable.real_const_sub
+ EIntegrable.smul_measure
+ EIntegrable.sub_const
+ EIntegrable.sub_real_const
+ EReal.enorm_ereal_toReal
+ EReal.posPart_fun_eq_zero_or_negPart_fun_eq_zero
+ EReal.posPart_fun_sub_negPart_fun
+ EReal.posPart_fun_sub_negPart_fun_apply
+ EReal.posPart_sub_negPart
+ Measurable.leOnePart'
+ Measurable.oneLePart'
+ ae_ne_bot_of_eintegral_ne_bot
+ ae_ne_top_of_eintegral_ne_top
+ coe_ennreal_le_coe_ennreal
+ eintegrable_add_of_ne_bot
+ eintegrable_congr
+ eintegrable_const
+ eintegrable_map
+ eintegrable_of_eintegral_ne_bot
+ eintegrable_of_le
+ eintegrable_of_nonneg
+ eintegrable_of_nonpos
+ eintegrable_zero
+ eintegral
+ eintegral_add
+ eintegral_add'
+ eintegral_add_compl
+ eintegral_add_measure
+ eintegral_add_ne_bot
+ eintegral_add_of_nonneg
+ eintegral_add_of_nonneg_ae
+ eintegral_add_of_nonneg_of_measurable'
+ eintegral_bind_of_nonneg
+ eintegral_coe_ennreal_sub
+ eintegral_comp_measure
+ eintegral_comp_measure_le
+ eintegral_congr
+ eintegral_congr_ae
+ eintegral_const
+ eintegral_const_mul
+ eintegral_dirac
+ eintegral_eq_integral
+ eintegral_eq_integral_toReal
+ eintegral_eq_lintegral
+ eintegral_eq_posPartFun_sub_negPartFun
+ eintegral_lt_top_of_le
+ eintegral_map
+ eintegral_map'
+ eintegral_mono
+ eintegral_mono_ae
+ eintegral_neg
+ eintegral_negPartFun_ne_top
+ eintegral_neg_eq_top_eq_bot
+ eintegral_nonneg
+ eintegral_nonneg'
+ eintegral_nonpos
+ eintegral_nonpos'
+ eintegral_of_ae_nonneg
+ eintegral_of_ae_nonpos
+ eintegral_of_nonneg
+ eintegral_of_nonpos
+ eintegral_of_not_eintegrable
+ eintegral_posPartFun_ne_top
+ eintegral_prod
+ eintegral_prod_of_nonneg
+ eintegral_prod_symm
+ eintegral_real_const_mul
+ eintegral_real_const_mul_of_nonneg
+ eintegral_smul_measure
+ eintegral_strict_mono
+ eintegral_strict_mono_ae
+ eintegral_sub
+ eintegral_sub'
+ eintegral_sub''
+ eintegral_sub_of_nonneg
+ eintegral_sub_of_nonneg_of_eq_zero
+ eintegral_sub_of_nonneg_of_eq_zero_ae
+ eintegral_zero
+ eintegral_zero_measure
+ instance : ENorm EReal
+ integrable_ereal_toReal_iff
+ integrable_toReal
+ lintegral_enorm_eq_posPartFun_add_negPartFun
+ lintegral_enorm_ereal_toReal
+ lintegral_eq_eintegral
+ one_le_leOnePart_fun
+ one_le_oneLePart_fun
+ setEIntegral_measure_zero

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 -- unavailable)

⚠️ The Mathlib cache for this PR's merge-base isn't on the server (typically a bors-batch intermediate that CI never built). Merge master into this PR and push to refresh.

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (6.00, 0.00)

Current number	Change	Type (weak)
5012	6	exposed public sections

Current commit e9f5d5d2b3
Reference commit e3b73828b0

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).

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat: lemmas about operations on EReal #41246
• [Merged by Bors] - chore: generalize instPosPart to SubNegMonoid #41247
• feat: variants of Measurable.oneLePart and related lemmas #41322
  By Dependent Issues (🤖). Happy coding!