Commit 2023-05-21 16:04 39893cc2

View on Github →

feat: port MeasureTheory.Function.SimpleFunc (#4043)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/SimpleFunc.lean

added theorem Measurable.ennreal_induction

added theorem MeasureTheory.SimpleFunc.FinMeasSupp.iff_lintegral_lt_top

added theorem MeasureTheory.SimpleFunc.FinMeasSupp.lintegral_lt_top

added theorem MeasureTheory.SimpleFunc.FinMeasSupp.map_iff

added theorem MeasureTheory.SimpleFunc.FinMeasSupp.meas_preimage_singleton_ne_zero

added theorem MeasureTheory.SimpleFunc.FinMeasSupp.of_lintegral_ne_top

added theorem MeasureTheory.SimpleFunc.FinMeasSupp.of_map

added theorem MeasureTheory.SimpleFunc.add_lintegral

added theorem MeasureTheory.SimpleFunc.apply_mk

added def MeasureTheory.SimpleFunc.approx

added theorem MeasureTheory.SimpleFunc.approx_apply

added theorem MeasureTheory.SimpleFunc.approx_comp

added def MeasureTheory.SimpleFunc.bind

added theorem MeasureTheory.SimpleFunc.bind_apply

added theorem MeasureTheory.SimpleFunc.bind_const

added theorem MeasureTheory.SimpleFunc.coe_comp

added theorem MeasureTheory.SimpleFunc.coe_const

added theorem MeasureTheory.SimpleFunc.coe_div

added theorem MeasureTheory.SimpleFunc.coe_inf

added theorem MeasureTheory.SimpleFunc.coe_injective

added theorem MeasureTheory.SimpleFunc.coe_inv

added theorem MeasureTheory.SimpleFunc.coe_le

added theorem MeasureTheory.SimpleFunc.coe_map

added theorem MeasureTheory.SimpleFunc.coe_mul

added theorem MeasureTheory.SimpleFunc.coe_one

added theorem MeasureTheory.SimpleFunc.coe_piecewise

added theorem MeasureTheory.SimpleFunc.coe_pow

added theorem MeasureTheory.SimpleFunc.coe_range

added theorem MeasureTheory.SimpleFunc.coe_restrict

added theorem MeasureTheory.SimpleFunc.coe_smul

added theorem MeasureTheory.SimpleFunc.coe_sup

added theorem MeasureTheory.SimpleFunc.coe_zpow

added def MeasureTheory.SimpleFunc.comp

added def MeasureTheory.SimpleFunc.const

added theorem MeasureTheory.SimpleFunc.const_apply

added theorem MeasureTheory.SimpleFunc.const_lintegral

added theorem MeasureTheory.SimpleFunc.const_lintegral_restrict

added theorem MeasureTheory.SimpleFunc.const_mul_eq_map

added theorem MeasureTheory.SimpleFunc.const_mul_lintegral

added theorem MeasureTheory.SimpleFunc.const_one

added theorem MeasureTheory.SimpleFunc.div_apply

added def MeasureTheory.SimpleFunc.eapprox

added def MeasureTheory.SimpleFunc.eapproxDiff

added theorem MeasureTheory.SimpleFunc.eapprox_comp

added theorem MeasureTheory.SimpleFunc.eapprox_lt_top

added def MeasureTheory.SimpleFunc.ennrealRatEmbed

added theorem MeasureTheory.SimpleFunc.ennrealRatEmbed_encode

added theorem MeasureTheory.SimpleFunc.eq_zero_of_mem_range_zero

added theorem MeasureTheory.SimpleFunc.exists_forall_le

added theorem MeasureTheory.SimpleFunc.exists_range_iff

added theorem MeasureTheory.SimpleFunc.ext

added def MeasureTheory.SimpleFunc.extend

added theorem MeasureTheory.SimpleFunc.extend_apply'

added theorem MeasureTheory.SimpleFunc.extend_apply

added theorem MeasureTheory.SimpleFunc.extend_comp_eq'

added theorem MeasureTheory.SimpleFunc.extend_comp_eq

added theorem MeasureTheory.SimpleFunc.finMeasSupp_iff

added theorem MeasureTheory.SimpleFunc.finMeasSupp_iff_support

added theorem MeasureTheory.SimpleFunc.finite_range

added theorem MeasureTheory.SimpleFunc.finset_sup_apply

added theorem MeasureTheory.SimpleFunc.forall_range_iff

added theorem MeasureTheory.SimpleFunc.iSup_approx_apply

added theorem MeasureTheory.SimpleFunc.iSup_eapprox_apply

added theorem MeasureTheory.SimpleFunc.inf_apply

added theorem MeasureTheory.SimpleFunc.inv_apply

added theorem MeasureTheory.SimpleFunc.le_sup_lintegral

added def MeasureTheory.SimpleFunc.lintegral

added theorem MeasureTheory.SimpleFunc.lintegral_add

added theorem MeasureTheory.SimpleFunc.lintegral_congr

added theorem MeasureTheory.SimpleFunc.lintegral_eq_of_measure_preimage

added theorem MeasureTheory.SimpleFunc.lintegral_eq_of_subset'

added theorem MeasureTheory.SimpleFunc.lintegral_eq_of_subset

added theorem MeasureTheory.SimpleFunc.lintegral_map'

added theorem MeasureTheory.SimpleFunc.lintegral_map

added theorem MeasureTheory.SimpleFunc.lintegral_mono

added theorem MeasureTheory.SimpleFunc.lintegral_restrict

added theorem MeasureTheory.SimpleFunc.lintegral_smul

added theorem MeasureTheory.SimpleFunc.lintegral_sum

added theorem MeasureTheory.SimpleFunc.lintegral_zero

added def MeasureTheory.SimpleFunc.lintegralₗ

added def MeasureTheory.SimpleFunc.map

added theorem MeasureTheory.SimpleFunc.map_apply

added theorem MeasureTheory.SimpleFunc.map_coe_ennreal_restrict

added theorem MeasureTheory.SimpleFunc.map_coe_nnreal_restrict

added theorem MeasureTheory.SimpleFunc.map_const

added theorem MeasureTheory.SimpleFunc.map_lintegral

added theorem MeasureTheory.SimpleFunc.map_map

added theorem MeasureTheory.SimpleFunc.map_mul

added theorem MeasureTheory.SimpleFunc.map_preimage

added theorem MeasureTheory.SimpleFunc.map_preimage_singleton

added theorem MeasureTheory.SimpleFunc.map_restrict_of_zero

added theorem MeasureTheory.SimpleFunc.measurableSet_cut

added theorem MeasureTheory.SimpleFunc.measurableSet_fiber

added theorem MeasureTheory.SimpleFunc.measurableSet_preimage

added theorem MeasureTheory.SimpleFunc.measurableSet_support

added theorem MeasureTheory.SimpleFunc.measurable_bind

added theorem MeasureTheory.SimpleFunc.mem_image_of_mem_range_restrict

added theorem MeasureTheory.SimpleFunc.mem_range

added theorem MeasureTheory.SimpleFunc.mem_range_of_measure_ne_zero

added theorem MeasureTheory.SimpleFunc.mem_range_self

added theorem MeasureTheory.SimpleFunc.mem_restrict_range

added theorem MeasureTheory.SimpleFunc.monotone_approx

added theorem MeasureTheory.SimpleFunc.monotone_eapprox

added theorem MeasureTheory.SimpleFunc.mul_apply

added theorem MeasureTheory.SimpleFunc.mul_eq_map₂

added def MeasureTheory.SimpleFunc.ofIsEmpty

added def MeasureTheory.SimpleFunc.pair

added theorem MeasureTheory.SimpleFunc.pair_apply

added theorem MeasureTheory.SimpleFunc.pair_preimage

added theorem MeasureTheory.SimpleFunc.pair_preimage_singleton

added def MeasureTheory.SimpleFunc.piecewise

added theorem MeasureTheory.SimpleFunc.piecewise_apply

added theorem MeasureTheory.SimpleFunc.piecewise_compl

added theorem MeasureTheory.SimpleFunc.piecewise_empty

added theorem MeasureTheory.SimpleFunc.piecewise_univ

added theorem MeasureTheory.SimpleFunc.pow_apply

added theorem MeasureTheory.SimpleFunc.preimage_eq_empty_iff

added theorem MeasureTheory.SimpleFunc.range_comp_subset_range

added theorem MeasureTheory.SimpleFunc.range_const

added theorem MeasureTheory.SimpleFunc.range_const_subset

added theorem MeasureTheory.SimpleFunc.range_eq_empty_of_isEmpty

added theorem MeasureTheory.SimpleFunc.range_indicator

added theorem MeasureTheory.SimpleFunc.range_map

added theorem MeasureTheory.SimpleFunc.range_one

added def MeasureTheory.SimpleFunc.restrict

added theorem MeasureTheory.SimpleFunc.restrict_apply

added theorem MeasureTheory.SimpleFunc.restrict_const_lintegral

added theorem MeasureTheory.SimpleFunc.restrict_empty

added theorem MeasureTheory.SimpleFunc.restrict_lintegral

added theorem MeasureTheory.SimpleFunc.restrict_lintegral_eq_lintegral_restrict

added theorem MeasureTheory.SimpleFunc.restrict_mono

added theorem MeasureTheory.SimpleFunc.restrict_of_not_measurable

added theorem MeasureTheory.SimpleFunc.restrict_preimage

added theorem MeasureTheory.SimpleFunc.restrict_preimage_singleton

added theorem MeasureTheory.SimpleFunc.restrict_univ

added def MeasureTheory.SimpleFunc.seq

added theorem MeasureTheory.SimpleFunc.seq_apply

added theorem MeasureTheory.SimpleFunc.simpleFunc_bot'

added theorem MeasureTheory.SimpleFunc.simpleFunc_bot

added theorem MeasureTheory.SimpleFunc.smul_apply

added theorem MeasureTheory.SimpleFunc.smul_eq_map

added theorem MeasureTheory.SimpleFunc.sum_eapproxDiff

added theorem MeasureTheory.SimpleFunc.sum_range_measure_preimage_singleton

added theorem MeasureTheory.SimpleFunc.sup_apply

added theorem MeasureTheory.SimpleFunc.sup_eq_map₂

added theorem MeasureTheory.SimpleFunc.support_eq

added theorem MeasureTheory.SimpleFunc.support_indicator

added theorem MeasureTheory.SimpleFunc.tsum_eapproxDiff

added theorem MeasureTheory.SimpleFunc.zero_lintegral

added theorem MeasureTheory.SimpleFunc.zpow_apply

added structure MeasureTheory.SimpleFunc.{u,