Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-06 22:45 f88234d1

View on Github →

feat(measure_theory): integral of a non-negative function is >0 iff μ(support f) > 0 (#4410) Also add a few supporting lemmas

Estimated changes

Modified src/algebra/order.lean

added theorem has_le.le.le_iff_eq

added theorem has_le.le.lt_iff_ne

Modified src/data/indicator_function.lean

added theorem set.indicator_of_support_subset

added theorem set.indicator_support

Modified src/data/support.lean

added theorem function.support_eq_empty_iff

Modified src/measure_theory/bochner_integration.lean

added theorem measure_theory.integral_eq_zero_iff_of_nonneg

added theorem measure_theory.integral_eq_zero_iff_of_nonneg_ae

added theorem measure_theory.integral_pos_iff_support_of_nonneg

added theorem measure_theory.integral_pos_iff_support_of_nonneg_ae

Modified src/measure_theory/integration.lean

modified theorem measure_theory.lintegral_eq_zero_iff

added theorem measure_theory.lintegral_pos_iff_support

Modified src/measure_theory/interval_integral.lean

added theorem interval_integral.integral_eq_integral_of_support_subset

added theorem interval_integral.integral_eq_zero_iff_of_le_of_nonneg_ae

added theorem interval_integral.integral_eq_zero_iff_of_nonneg_ae

added theorem interval_integral.integral_non_measurable

added theorem interval_integral.integral_pos_iff_support_of_nonneg_ae'

added theorem interval_integral.integral_pos_iff_support_of_nonneg_ae

added theorem interval_integral.integral_zero

added theorem measure_theory.integrable.interval_integrable

Modified src/measure_theory/lebesgue_measure.lean

added theorem filter.eventually.volume_pos_of_nhds_real

Modified src/measure_theory/set_integral.lean

added theorem continuous.integrable_of_compact_closure_support

added theorem measure_theory.set_integral_eq_zero_iff_of_nonneg_ae

added theorem measure_theory.set_integral_pos_iff_support_of_nonneg_ae

Modified src/order/filter/basic.lean

added theorem filter.eventually_le.le_iff_eq

Modified src/topology/algebra/ordered.lean

added theorem filter.eventually.exists_Ioo_subset

Modified src/topology/basic.lean

added theorem is_open.eventually_mem