mathlib

1e46532c - feat(measure_theory/integral/lebesgue): `lintegral_add` holds if 1 function is measurable (#14278)

feat(measure_theory/integral/lebesgue): `lintegral_add` holds if 1 function is measurable (#14278) * for any function `f` there exists a measurable function `g ≤ f` with the same Lebesgue integral; * prove `∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ` assuming **one** of the functions is (a.e.-)measurable; split `lintegral_add` into two lemmas `lintegral_add_(left|right)`; * prove `∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ ≤ ∫⁻ a, f a + g a ∂μ` for any `f`, `g`; * prove a version of Markov's inequality for `μ {x | f x + ε ≤ g x}` with possibly non-measurable `f`; * prove `f ≤ᵐ[μ] g → ∫⁻ x, f x ∂μ ≠ ∞ → ∫⁻ x, g x ∂μ ≤ ∫⁻ x, f x ∂μ → f =ᵐ[μ] g` for an a.e.-measurable function `f`; * drop one measurability assumption in `lintegral_sub` and `lintegral_sub_le`; * add `lintegral_strict_mono_of_ae_le_of_frequently_ae_lt`, a version of `lintegral_strict_mono_of_ae_le_of_ae_lt_on`; * drop one measurability assumption in `lintegral_strict_mono_of_ae_le_of_ae_lt_on`, `lintegral_strict_mono`, and `set_lintegral_strict_mono`; * prove `with_density_add` assuming measurability of one of the functions; replace it with `with_density_add_(left|right)`; * drop measurability assumptions here and there in `mean_inequalities`.