Commit 2023-06-06 04:38 aecdd161

View on Github →

feat: port MeasureTheory.Function.AEEqOfIntegral (#4711)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

added theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_of_forall_set_integral_eq

added theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_of_forall_set_integral_eq_zero

added theorem MeasureTheory.AEFinStronglyMeasurable.ae_nonneg_of_forall_set_integral_nonneg

added theorem MeasureTheory.AeMeasurable.ae_eq_of_forall_set_lintegral_eq

added theorem MeasureTheory.Integrable.ae_eq_of_forall_set_integral_eq

added theorem MeasureTheory.Integrable.ae_eq_zero_of_forall_set_integral_eq_zero

added theorem MeasureTheory.Lp.ae_eq_of_forall_set_integral_eq

added theorem MeasureTheory.Lp.ae_eq_zero_of_forall_set_integral_eq_zero

added theorem MeasureTheory.ae_const_le_iff_forall_lt_measure_zero

added theorem MeasureTheory.ae_eq_of_forall_set_integral_eq_of_sigmaFinite

added theorem MeasureTheory.ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite

added theorem MeasureTheory.ae_eq_restrict_of_forall_set_integral_eq

added theorem MeasureTheory.ae_eq_zero_of_forall_dual

added theorem MeasureTheory.ae_eq_zero_of_forall_dual_of_isSeparable

added theorem MeasureTheory.ae_eq_zero_of_forall_inner

added theorem MeasureTheory.ae_eq_zero_of_forall_set_integral_eq_of_finStronglyMeasurable_trim

added theorem MeasureTheory.ae_eq_zero_of_forall_set_integral_eq_of_sigmaFinite

added theorem MeasureTheory.ae_eq_zero_restrict_of_forall_set_integral_eq_zero

added theorem MeasureTheory.ae_eq_zero_restrict_of_forall_set_integral_eq_zero_real

added theorem MeasureTheory.ae_le_of_forall_set_integral_le

added theorem MeasureTheory.ae_le_of_forall_set_lintegral_le_of_sigmaFinite

added theorem MeasureTheory.ae_nonneg_of_forall_set_integral_nonneg

added theorem MeasureTheory.ae_nonneg_of_forall_set_integral_nonneg_of_sigmaFinite

added theorem MeasureTheory.ae_nonneg_of_forall_set_integral_nonneg_of_stronglyMeasurable

added theorem MeasureTheory.ae_nonneg_restrict_of_forall_set_integral_nonneg

added theorem MeasureTheory.ae_nonneg_restrict_of_forall_set_integral_nonneg_inter