Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-28 11:35 c04a42fe

View on Github →

feat(measure_theory/integral/{interval,circle}_integral): add strict inequalities (#11061)

Estimated changes

Modified src/measure_theory/integral/circle_integral.lean

added theorem circle_integral.norm_integral_lt_of_norm_le_const_of_lt

added theorem circle_integral.norm_two_pi_I_inv_smul_integral_le_of_norm_le_const

Modified src/measure_theory/integral/interval_integral.lean

modified theorem interval_integral.abs_integral_le_integral_abs

added theorem interval_integral.integral_lt_integral_of_ae_le_of_measure_set_of_lt_ne_zero

added theorem interval_integral.integral_lt_integral_of_continuous_on_of_le_of_exists_lt

modified theorem interval_integral.integral_nonneg_of_ae

modified theorem interval_integral.integral_nonneg_of_ae_restrict

modified theorem interval_integral.integral_nonneg_of_forall

modified theorem interval_integral.integral_pos_iff_support_of_nonneg_ae