Commit 2023-06-07 06:21 5e32f284

View on Github →

feat: port MeasureTheory.Integral.IntervalIntegral (#4710)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

added theorem Antitone.intervalIntegrable

added theorem AntitoneOn.intervalIntegrable

added theorem Continuous.intervalIntegrable

added theorem ContinuousLinearMap.intervalIntegral_apply

added theorem ContinuousLinearMap.intervalIntegral_comp_comm

added theorem ContinuousOn.intervalIntegrable

added theorem ContinuousOn.intervalIntegrable_of_Icc

added theorem Filter.Tendsto.eventually_intervalIntegrable

added theorem Filter.Tendsto.eventually_intervalIntegrable_ae

added theorem IntervalIntegrable.abs

added theorem IntervalIntegrable.add

added theorem IntervalIntegrable.comp_add_left

added theorem IntervalIntegrable.comp_add_right

added theorem IntervalIntegrable.comp_mul_left

added theorem IntervalIntegrable.comp_mul_left_iff

added theorem IntervalIntegrable.comp_mul_right

added theorem IntervalIntegrable.comp_sub_left

added theorem IntervalIntegrable.comp_sub_right

added theorem IntervalIntegrable.const_mul

added theorem IntervalIntegrable.continuousOn_mul

added theorem IntervalIntegrable.def

added theorem IntervalIntegrable.div_const

added theorem IntervalIntegrable.iff_comp_neg

added theorem IntervalIntegrable.intervalIntegrable_norm_iff

added theorem IntervalIntegrable.mono

added theorem IntervalIntegrable.mono_fun'

added theorem IntervalIntegrable.mono_fun

added theorem IntervalIntegrable.mono_measure

added theorem IntervalIntegrable.mono_set'

added theorem IntervalIntegrable.mono_set

added theorem IntervalIntegrable.mono_set_ae

added theorem IntervalIntegrable.mul_const

added theorem IntervalIntegrable.mul_continuousOn

added theorem IntervalIntegrable.neg

added theorem IntervalIntegrable.norm

added theorem IntervalIntegrable.refl

added theorem IntervalIntegrable.smul

added theorem IntervalIntegrable.sub

added theorem IntervalIntegrable.sum

added theorem IntervalIntegrable.trans

added theorem IntervalIntegrable.trans_iterate

added theorem IntervalIntegrable.trans_iterate_Ico

added def IntervalIntegrable

added theorem MeasureTheory.Integrable.hasSum_intervalIntegral

added theorem MeasureTheory.Integrable.hasSum_intervalIntegral_comp_add_int

added theorem MeasureTheory.Integrable.intervalIntegrable

added theorem MeasureTheory.IntegrableOn.intervalIntegrable

added theorem Monotone.intervalIntegrable

added theorem MonotoneOn.intervalIntegrable

added theorem intervalIntegrable_const

added theorem intervalIntegrable_const_iff

added theorem intervalIntegrable_iff'

added theorem intervalIntegrable_iff

added theorem intervalIntegrable_iff_integrable_Icc_of_le

added theorem intervalIntegrable_iff_integrable_Ioc_of_le

added theorem intervalIntegral.abs_integral_eq_abs_integral_uIoc

added theorem intervalIntegral.abs_integral_le_integral_abs

added theorem intervalIntegral.abs_integral_mono_interval

added theorem intervalIntegral.abs_intervalIntegral_eq

added theorem intervalIntegral.continuousAt_of_dominated_interval

added theorem intervalIntegral.continuousOn_primitive

added theorem intervalIntegral.continuousOn_primitive_Icc

added theorem intervalIntegral.continuousOn_primitive_interval'

added theorem intervalIntegral.continuousOn_primitive_interval

added theorem intervalIntegral.continuousOn_primitive_interval_left

added theorem intervalIntegral.continuousWithinAt_of_dominated_interval

added theorem intervalIntegral.continuousWithinAt_primitive

added theorem intervalIntegral.continuous_of_dominated_interval

added theorem intervalIntegral.continuous_primitive

added theorem intervalIntegral.hasSum_intervalIntegral_of_summable_norm

added theorem intervalIntegral.integral_Iic_sub_Iic

added theorem intervalIntegral.integral_add_adjacent_intervals

added theorem intervalIntegral.integral_add_adjacent_intervals_cancel

added theorem intervalIntegral.integral_cases

added theorem intervalIntegral.integral_comp_add_div

added theorem intervalIntegral.integral_comp_add_mul

added theorem intervalIntegral.integral_comp_add_right

added theorem intervalIntegral.integral_comp_div

added theorem intervalIntegral.integral_comp_div_add

added theorem intervalIntegral.integral_comp_div_sub

added theorem intervalIntegral.integral_comp_mul_add

added theorem intervalIntegral.integral_comp_mul_left

added theorem intervalIntegral.integral_comp_mul_right

added theorem intervalIntegral.integral_comp_mul_sub

added theorem intervalIntegral.integral_comp_neg

added theorem intervalIntegral.integral_comp_sub_div

added theorem intervalIntegral.integral_comp_sub_left

added theorem intervalIntegral.integral_comp_sub_mul

added theorem intervalIntegral.integral_comp_sub_right

added theorem intervalIntegral.integral_congr

added theorem intervalIntegral.integral_congr_ae'

added theorem intervalIntegral.integral_congr_ae

added theorem intervalIntegral.integral_const'

added theorem intervalIntegral.integral_const

added theorem intervalIntegral.integral_const_mul

added theorem intervalIntegral.integral_const_of_cdf

added theorem intervalIntegral.integral_div

added theorem intervalIntegral.integral_eq_integral_of_support_subset

added theorem intervalIntegral.integral_eq_zero_iff_of_le_of_nonneg_ae

added theorem intervalIntegral.integral_eq_zero_iff_of_nonneg_ae

added theorem intervalIntegral.integral_interval_add_interval_comm

added theorem intervalIntegral.integral_interval_sub_interval_comm'

added theorem intervalIntegral.integral_interval_sub_interval_comm

added theorem intervalIntegral.integral_interval_sub_left

added theorem intervalIntegral.integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero

added theorem intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt

added theorem intervalIntegral.integral_mono

added theorem intervalIntegral.integral_mono_ae

added theorem intervalIntegral.integral_mono_ae_restrict

added theorem intervalIntegral.integral_mono_interval

added theorem intervalIntegral.integral_mono_on

added theorem intervalIntegral.integral_mul_const

added theorem intervalIntegral.integral_non_aestronglyMeasurable_of_le

added theorem intervalIntegral.integral_nonneg

added theorem intervalIntegral.integral_nonneg_of_ae

added theorem intervalIntegral.integral_nonneg_of_ae_restrict

added theorem intervalIntegral.integral_nonneg_of_forall

added theorem intervalIntegral.integral_of_ge

added theorem intervalIntegral.integral_of_le

added theorem intervalIntegral.integral_pos_iff_support_of_nonneg_ae'

added theorem intervalIntegral.integral_pos_iff_support_of_nonneg_ae

added theorem intervalIntegral.integral_same

added theorem intervalIntegral.integral_sub

added theorem intervalIntegral.integral_symm

added theorem intervalIntegral.integral_zero

added theorem intervalIntegral.integral_zero_ae

added theorem intervalIntegral.intervalIntegrable_of_integral_ne_zero

added theorem intervalIntegral.intervalIntegral_eq_integral_uIoc

added theorem intervalIntegral.intervalIntegral_pos_of_pos

added theorem intervalIntegral.intervalIntegral_pos_of_pos_on

added theorem intervalIntegral.inv_smul_integral_comp_add_div

added theorem intervalIntegral.inv_smul_integral_comp_div

added theorem intervalIntegral.inv_smul_integral_comp_div_add

added theorem intervalIntegral.inv_smul_integral_comp_div_sub

added theorem intervalIntegral.inv_smul_integral_comp_sub_div

added theorem intervalIntegral.norm_integral_eq_norm_integral_Ioc

added theorem intervalIntegral.norm_integral_le_abs_integral_norm

added theorem intervalIntegral.norm_integral_le_integral_norm

added theorem intervalIntegral.norm_integral_le_integral_norm_Ioc

added theorem intervalIntegral.norm_integral_le_of_norm_le_const

added theorem intervalIntegral.norm_integral_le_of_norm_le_const_ae

added theorem intervalIntegral.norm_integral_min_max

added theorem intervalIntegral.norm_intervalIntegral_eq

added theorem intervalIntegral.smul_integral_comp_add_mul

added theorem intervalIntegral.smul_integral_comp_mul_add

added theorem intervalIntegral.smul_integral_comp_mul_left

added theorem intervalIntegral.smul_integral_comp_mul_right

added theorem intervalIntegral.smul_integral_comp_mul_sub

added theorem intervalIntegral.smul_integral_comp_sub_mul

added theorem intervalIntegral.sum_integral_adjacent_intervals

added theorem intervalIntegral.sum_integral_adjacent_intervals_Ico

added theorem intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm

added def intervalIntegral

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

added theorem integral_ofReal

deleted theorem integral_of_real