Commit 2023-05-21 17:05 28e1d299

View on Github →

feat: port MeasureTheory.Integral.Lebesgue (#4058)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/Lebesgue.lean

added theorem ENNReal.count_const_le_le_of_tsum_le

added theorem ENNReal.tsum_const_eq

added theorem IsFiniteMeasure.lintegral_lt_top_of_bounded_to_eNNReal

added theorem MeasurableEmbedding.lintegral_map

added def MeasureTheory.Measure.withDensity

added theorem MeasureTheory.MeasurePreserving.lintegral_comp

added theorem MeasureTheory.MeasurePreserving.lintegral_comp_emb

added theorem MeasureTheory.MeasurePreserving.set_lintegral_comp_emb

added theorem MeasureTheory.MeasurePreserving.set_lintegral_comp_preimage

added theorem MeasureTheory.MeasurePreserving.set_lintegral_comp_preimage_emb

added theorem MeasureTheory.SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral

added theorem MeasureTheory.SimpleFunc.lintegral_eq_lintegral

added theorem MeasureTheory.aEMeasurable_withDensity_eNNReal_iff

added theorem MeasureTheory.ae_eq_of_ae_le_of_lintegral_le

added theorem MeasureTheory.ae_lt_top'

added theorem MeasureTheory.ae_lt_top

added theorem MeasureTheory.ae_withDensity_iff

added theorem MeasureTheory.ae_withDensity_iff_ae_restrict

added theorem MeasureTheory.exists_absolutelyContinuous_finiteMeasure

added theorem MeasureTheory.exists_lt_lintegral_simpleFunc_of_lt_lintegral

added theorem MeasureTheory.exists_measurable_le_lintegral_eq

added theorem MeasureTheory.exists_pos_lintegral_lt_of_sigmaFinite

added theorem MeasureTheory.exists_pos_set_lintegral_lt_of_measure_lt

added theorem MeasureTheory.exists_simpleFunc_forall_lintegral_sub_lt_of_pos

added theorem MeasureTheory.finiteMeasure_withDensity

added theorem MeasureTheory.hasSum_lintegral_measure

added theorem MeasureTheory.iSup_lintegral_le

added theorem MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral

added theorem MeasureTheory.iSup₂_lintegral_le

added theorem MeasureTheory.le_iInf_lintegral

added theorem MeasureTheory.le_iInf₂_lintegral

added theorem MeasureTheory.le_lintegral_add

added theorem MeasureTheory.limsup_lintegral_le

added theorem MeasureTheory.lintegral_add_aux

added theorem MeasureTheory.lintegral_add_compl

added theorem MeasureTheory.lintegral_add_left'

added theorem MeasureTheory.lintegral_add_left

added theorem MeasureTheory.lintegral_add_measure

added theorem MeasureTheory.lintegral_add_mul_meas_add_le_le_lintegral

added theorem MeasureTheory.lintegral_add_right'

added theorem MeasureTheory.lintegral_add_right

added theorem MeasureTheory.lintegral_biUnion

added theorem MeasureTheory.lintegral_biUnion_finset

added theorem MeasureTheory.lintegral_biUnion_finset₀

added theorem MeasureTheory.lintegral_biUnion₀

added theorem MeasureTheory.lintegral_comp

added theorem MeasureTheory.lintegral_congr

added theorem MeasureTheory.lintegral_congr_ae

added theorem MeasureTheory.lintegral_const

added theorem MeasureTheory.lintegral_const_lt_top

added theorem MeasureTheory.lintegral_const_mul''

added theorem MeasureTheory.lintegral_const_mul'

added theorem MeasureTheory.lintegral_const_mul

added theorem MeasureTheory.lintegral_const_mul_le

added theorem MeasureTheory.lintegral_count'

added theorem MeasureTheory.lintegral_count

added theorem MeasureTheory.lintegral_countable'

added theorem MeasureTheory.lintegral_countable

added theorem MeasureTheory.lintegral_dirac'

added theorem MeasureTheory.lintegral_dirac

added theorem MeasureTheory.lintegral_eq_iSup_eapprox_lintegral

added theorem MeasureTheory.lintegral_eq_nnreal

added theorem MeasureTheory.lintegral_eq_top_of_measure_eq_top_pos

added theorem MeasureTheory.lintegral_eq_zero_iff'

added theorem MeasureTheory.lintegral_eq_zero_iff

added theorem MeasureTheory.lintegral_finset

added theorem MeasureTheory.lintegral_finset_sum'

added theorem MeasureTheory.lintegral_finset_sum

added theorem MeasureTheory.lintegral_finset_sum_measure

added theorem MeasureTheory.lintegral_fintype

added theorem MeasureTheory.lintegral_iInf

added theorem MeasureTheory.lintegral_iInf_ae

added theorem MeasureTheory.lintegral_iSup'

added theorem MeasureTheory.lintegral_iSup

added theorem MeasureTheory.lintegral_iSup_ae

added theorem MeasureTheory.lintegral_iSup_directed

added theorem MeasureTheory.lintegral_iSup_directed_of_measurable

added theorem MeasureTheory.lintegral_iUnion

added theorem MeasureTheory.lintegral_iUnion_le

added theorem MeasureTheory.lintegral_iUnion₀

added theorem MeasureTheory.lintegral_indicator

added theorem MeasureTheory.lintegral_indicator_const

added theorem MeasureTheory.lintegral_indicator_const_comp

added theorem MeasureTheory.lintegral_indicator₀

added theorem MeasureTheory.lintegral_insert

added theorem MeasureTheory.lintegral_inter_add_diff

added theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le'

added theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le

added theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le_of_measurable

added theorem MeasureTheory.lintegral_liminf_le'

added theorem MeasureTheory.lintegral_liminf_le

added theorem MeasureTheory.lintegral_lintegral_mul

added theorem MeasureTheory.lintegral_map'

added theorem MeasureTheory.lintegral_map

added theorem MeasureTheory.lintegral_map_equiv

added theorem MeasureTheory.lintegral_map_le

added theorem MeasureTheory.lintegral_max

added theorem MeasureTheory.lintegral_mono'

added theorem MeasureTheory.lintegral_mono

added theorem MeasureTheory.lintegral_mono_ae

added theorem MeasureTheory.lintegral_mono_nnreal

added theorem MeasureTheory.lintegral_mono_set'

added theorem MeasureTheory.lintegral_mono_set

added theorem MeasureTheory.lintegral_mul_const''

added theorem MeasureTheory.lintegral_mul_const'

added theorem MeasureTheory.lintegral_mul_const

added theorem MeasureTheory.lintegral_mul_const_le

added theorem MeasureTheory.lintegral_nnnorm_eq_of_ae_nonneg

added theorem MeasureTheory.lintegral_nnnorm_eq_of_nonneg

added theorem MeasureTheory.lintegral_ofReal_le_lintegral_nnnorm

added theorem MeasureTheory.lintegral_one

added theorem MeasureTheory.lintegral_pos_iff_support

added theorem MeasureTheory.lintegral_rw₁

added theorem MeasureTheory.lintegral_rw₂

added theorem MeasureTheory.lintegral_singleton'

added theorem MeasureTheory.lintegral_singleton

added theorem MeasureTheory.lintegral_smul_measure

added theorem MeasureTheory.lintegral_strict_mono

added theorem MeasureTheory.lintegral_strict_mono_of_ae_le_of_ae_lt_on

added theorem MeasureTheory.lintegral_strict_mono_of_ae_le_of_frequently_ae_lt

added theorem MeasureTheory.lintegral_sub'

added theorem MeasureTheory.lintegral_sub

added theorem MeasureTheory.lintegral_sub_le'

added theorem MeasureTheory.lintegral_sub_le

added theorem MeasureTheory.lintegral_sum_measure

added theorem MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone

added theorem MeasureTheory.lintegral_trim

added theorem MeasureTheory.lintegral_trim_ae

added theorem MeasureTheory.lintegral_tsum

added theorem MeasureTheory.lintegral_union

added theorem MeasureTheory.lintegral_unique

added theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul

added theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable

added theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable₀

added theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀'

added theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀

added theorem MeasureTheory.lintegral_withDensity_le_lintegral_mul

added theorem MeasureTheory.lintegral_zero

added theorem MeasureTheory.lintegral_zero_fun

added theorem MeasureTheory.lintegral_zero_measure

added theorem MeasureTheory.meas_ge_le_lintegral_div

added theorem MeasureTheory.monotone_lintegral

added theorem MeasureTheory.mul_meas_ge_le_lintegral

added theorem MeasureTheory.mul_meas_ge_le_lintegral₀

added theorem MeasureTheory.restrict_dirac'

added theorem MeasureTheory.restrict_dirac

added theorem MeasureTheory.restrict_withDensity

added theorem MeasureTheory.set_lintegral_congr

added theorem MeasureTheory.set_lintegral_congr_fun

added theorem MeasureTheory.set_lintegral_const

added theorem MeasureTheory.set_lintegral_const_lt_top

added theorem MeasureTheory.set_lintegral_dirac'

added theorem MeasureTheory.set_lintegral_dirac

added theorem MeasureTheory.set_lintegral_empty

added theorem MeasureTheory.set_lintegral_eq_const

added theorem MeasureTheory.set_lintegral_lt_top_of_bddAbove

added theorem MeasureTheory.set_lintegral_lt_top_of_isCompact

added theorem MeasureTheory.set_lintegral_map

added theorem MeasureTheory.set_lintegral_max

added theorem MeasureTheory.set_lintegral_measure_zero

added theorem MeasureTheory.set_lintegral_mono

added theorem MeasureTheory.set_lintegral_mono_ae

added theorem MeasureTheory.set_lintegral_one

added theorem MeasureTheory.set_lintegral_strict_mono

added theorem MeasureTheory.set_lintegral_univ

added theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul

added theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable

added theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀

added theorem MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence

added theorem MeasureTheory.tendsto_lintegral_of_dominated_convergence'

added theorem MeasureTheory.tendsto_lintegral_of_dominated_convergence

added theorem MeasureTheory.tendsto_set_lintegral_zero

added theorem MeasureTheory.univ_le_of_forall_fin_meas_le

added theorem MeasureTheory.withDensity_absolutelyContinuous

added theorem MeasureTheory.withDensity_add_left

added theorem MeasureTheory.withDensity_add_measure

added theorem MeasureTheory.withDensity_add_right

added theorem MeasureTheory.withDensity_apply

added theorem MeasureTheory.withDensity_apply_eq_zero

added theorem MeasureTheory.withDensity_congr_ae

added theorem MeasureTheory.withDensity_eq_zero

added theorem MeasureTheory.withDensity_indicator

added theorem MeasureTheory.withDensity_indicator_one

added theorem MeasureTheory.withDensity_mul

added theorem MeasureTheory.withDensity_ofReal_mutuallySingular

added theorem MeasureTheory.withDensity_one

added theorem MeasureTheory.withDensity_smul'

added theorem MeasureTheory.withDensity_smul

added theorem MeasureTheory.withDensity_sum

added theorem MeasureTheory.withDensity_tsum

added theorem MeasureTheory.withDensity_zero

added theorem NNReal.count_const_le_le_of_tsum_le

added def unexpandLIntegral