Commit 2022-05-28 15:49 1e46532c

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.