Commit 2023-06-06 00:38 7d6d728f

View on Github →

feat: port MeasureTheory.Integral.SetIntegral (#4690)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/SetIntegral.lean

added theorem Antitone.tendsto_set_integral

added theorem ClosedEmbedding.set_integral_map

added theorem ContinuousAt.integral_sub_linear_isLittleO_ae

added theorem ContinuousLinearEquiv.integral_comp_comm

added theorem ContinuousLinearMap.continuous_integral_comp_L1

added theorem ContinuousLinearMap.integral_apply

added theorem ContinuousLinearMap.integral_compLp

added theorem ContinuousLinearMap.integral_comp_L1_comm

added theorem ContinuousLinearMap.integral_comp_comm'

added theorem ContinuousLinearMap.integral_comp_comm

added theorem ContinuousLinearMap.set_integral_compLp

added theorem ContinuousOn.integral_sub_linear_isLittleO_ae

added theorem ContinuousWithinAt.integral_sub_linear_isLittleO_ae

added theorem Filter.Tendsto.integral_sub_linear_isLittleO_ae

added theorem LinearIsometry.integral_comp_comm

added theorem MeasurableEmbedding.set_integral_map

added theorem MeasureTheory.Integrable.simpleFunc_mul'

added theorem MeasureTheory.Integrable.simpleFunc_mul

added def MeasureTheory.LpToLpRestrictCLM

added theorem MeasureTheory.LpToLpRestrictCLM_coeFn

added theorem MeasureTheory.Lp_toLp_restrict_add

added theorem MeasureTheory.Lp_toLp_restrict_smul

added theorem MeasureTheory.MeasurePreserving.set_integral_image_emb

added theorem MeasureTheory.MeasurePreserving.set_integral_preimage_emb

added theorem MeasureTheory.continuous_set_integral

added theorem MeasureTheory.hasSum_integral_iUnion

added theorem MeasureTheory.hasSum_integral_iUnion_ae

added theorem MeasureTheory.integrableOn_iUnion_of_summable_integral_norm

added theorem MeasureTheory.integrableOn_iUnion_of_summable_norm_restrict

added theorem MeasureTheory.integrable_of_summable_norm_restrict

added theorem MeasureTheory.integral_Icc_eq_integral_Ico'

added theorem MeasureTheory.integral_Icc_eq_integral_Ico

added theorem MeasureTheory.integral_Icc_eq_integral_Ioc'

added theorem MeasureTheory.integral_Icc_eq_integral_Ioc

added theorem MeasureTheory.integral_Icc_eq_integral_Ioo'

added theorem MeasureTheory.integral_Icc_eq_integral_Ioo

added theorem MeasureTheory.integral_Ici_eq_integral_Ioi'

added theorem MeasureTheory.integral_Ici_eq_integral_Ioi

added theorem MeasureTheory.integral_Ico_eq_integral_Ioo'

added theorem MeasureTheory.integral_Ico_eq_integral_Ioo

added theorem MeasureTheory.integral_Iic_eq_integral_Iio'

added theorem MeasureTheory.integral_Iic_eq_integral_Iio

added theorem MeasureTheory.integral_Ioc_eq_integral_Ioo'

added theorem MeasureTheory.integral_Ioc_eq_integral_Ioo

added theorem MeasureTheory.integral_add_compl

added theorem MeasureTheory.integral_add_compl₀

added theorem MeasureTheory.integral_diff

added theorem MeasureTheory.integral_empty

added theorem MeasureTheory.integral_finset_biUnion

added theorem MeasureTheory.integral_fintype_iUnion

added theorem MeasureTheory.integral_iUnion

added theorem MeasureTheory.integral_iUnion_ae

added theorem MeasureTheory.integral_indicator

added theorem MeasureTheory.integral_indicatorConstLp

added theorem MeasureTheory.integral_indicator_const

added theorem MeasureTheory.integral_indicator_one

added theorem MeasureTheory.integral_inter_add_diff

added theorem MeasureTheory.integral_inter_add_diff₀

added theorem MeasureTheory.integral_norm_eq_pos_sub_neg

added theorem MeasureTheory.integral_piecewise

added theorem MeasureTheory.integral_union

added theorem MeasureTheory.integral_union_ae

added theorem MeasureTheory.integral_union_eq_left_of_ae

added theorem MeasureTheory.integral_union_eq_left_of_ae_aux

added theorem MeasureTheory.integral_union_eq_left_of_forall

added theorem MeasureTheory.integral_union_eq_left_of_forall₀

added theorem MeasureTheory.integral_univ

added theorem MeasureTheory.norm_Lp_toLp_restrict_le

added theorem MeasureTheory.norm_set_integral_le_of_norm_le_const'

added theorem MeasureTheory.norm_set_integral_le_of_norm_le_const

added theorem MeasureTheory.norm_set_integral_le_of_norm_le_const_ae''

added theorem MeasureTheory.norm_set_integral_le_of_norm_le_const_ae'

added theorem MeasureTheory.norm_set_integral_le_of_norm_le_const_ae

added theorem MeasureTheory.ofReal_set_integral_one

added theorem MeasureTheory.ofReal_set_integral_one_of_measure_ne_top

added theorem MeasureTheory.set_integral_congr

added theorem MeasureTheory.set_integral_congr_ae

added theorem MeasureTheory.set_integral_congr_ae₀

added theorem MeasureTheory.set_integral_congr_set_ae

added theorem MeasureTheory.set_integral_congr₀

added theorem MeasureTheory.set_integral_const

added theorem MeasureTheory.set_integral_eq_integral_of_ae_compl_eq_zero

added theorem MeasureTheory.set_integral_eq_integral_of_forall_compl_eq_zero

added theorem MeasureTheory.set_integral_eq_of_subset_of_ae_diff_eq_zero

added theorem MeasureTheory.set_integral_eq_of_subset_of_ae_diff_eq_zero_aux

added theorem MeasureTheory.set_integral_eq_of_subset_of_forall_diff_eq_zero

added theorem MeasureTheory.set_integral_eq_zero_iff_of_nonneg_ae

added theorem MeasureTheory.set_integral_eq_zero_of_ae_eq_zero

added theorem MeasureTheory.set_integral_eq_zero_of_forall_eq_zero

added theorem MeasureTheory.set_integral_ge_of_const_le

added theorem MeasureTheory.set_integral_gt_gt

added theorem MeasureTheory.set_integral_indicator

added theorem MeasureTheory.set_integral_indicatorConstLp

added theorem MeasureTheory.set_integral_le_nonneg

added theorem MeasureTheory.set_integral_map

added theorem MeasureTheory.set_integral_map_equiv

added theorem MeasureTheory.set_integral_mono

added theorem MeasureTheory.set_integral_mono_ae

added theorem MeasureTheory.set_integral_mono_ae_restrict

added theorem MeasureTheory.set_integral_mono_on

added theorem MeasureTheory.set_integral_mono_on_ae

added theorem MeasureTheory.set_integral_mono_set

added theorem MeasureTheory.set_integral_neg_eq_set_integral_nonpos

added theorem MeasureTheory.set_integral_nonneg

added theorem MeasureTheory.set_integral_nonneg_ae

added theorem MeasureTheory.set_integral_nonneg_of_ae

added theorem MeasureTheory.set_integral_nonneg_of_ae_restrict

added theorem MeasureTheory.set_integral_nonpos

added theorem MeasureTheory.set_integral_nonpos_ae

added theorem MeasureTheory.set_integral_nonpos_le

added theorem MeasureTheory.set_integral_nonpos_of_ae

added theorem MeasureTheory.set_integral_nonpos_of_ae_restrict

added theorem MeasureTheory.set_integral_pos_iff_support_of_nonneg_ae

added theorem MeasureTheory.set_integral_trim

added theorem MeasureTheory.tendsto_set_integral_of_monotone

added theorem fst_integral

added theorem integral_coe_re_add_coe_im

added theorem integral_conj

added theorem integral_im

added theorem integral_of_real

added theorem integral_pair

added theorem integral_re

added theorem integral_re_add_im

added theorem integral_smul_const

added theorem integral_withDensity_eq_integral_smul

added theorem integral_withDensity_eq_integral_smul₀

added theorem measure_le_lintegral_thickenedIndicator

added theorem measure_le_lintegral_thickenedIndicatorAux

added theorem set_integral_re_add_im

added theorem set_integral_withDensity_eq_set_integral_smul

added theorem set_integral_withDensity_eq_set_integral_smul₀

added theorem snd_integral