Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-10 22:50 40f55657

View on Github →

feat(analysis/measure_theory): lower Lebesgue integral under addition, supremum

Estimated changes

Modified algebra/big_operators.lean

added theorem finset.prod_hom_rel

added theorem finset.prod_image'

Modified analysis/ennreal.lean

deleted theorem ennreal.coe_nat

added theorem ennreal.finset_sum_supr_nat

added theorem ennreal.mul_Sup

added theorem ennreal.mul_supr

modified theorem ennreal.supr_add_supr

added theorem ennreal.supr_add_supr_of_monotone

added theorem ennreal.supr_mul

added theorem ennreal.tendsto_coe_nnreal_nhds_top

Modified analysis/measure_theory/borel_space.lean

added theorem measure_theory.measurable_coe_int_real

added theorem measure_theory.measurable_le

Modified analysis/measure_theory/integration.lean

deleted def measure_theory.indicator.size

deleted def measure_theory.indicator.to_fun

deleted theorem measure_theory.indicator.to_fun_val

deleted structure measure_theory.indicator

added def measure_theory.lintegral

added theorem measure_theory.lintegral_add

added theorem measure_theory.lintegral_eq_nnreal

added theorem measure_theory.lintegral_eq_supr_eapprox_integral

added theorem measure_theory.lintegral_le_lintegral

added theorem measure_theory.lintegral_supr

added theorem measure_theory.lintegral_zero

deleted def measure_theory.simple_func'.bind

deleted theorem measure_theory.simple_func'.bind_apply

deleted theorem measure_theory.simple_func'.bind_const

deleted theorem measure_theory.simple_func'.bind_itg

deleted theorem measure_theory.simple_func'.bind_sum_measure

deleted theorem measure_theory.simple_func'.coe_def

deleted theorem measure_theory.simple_func'.coe_le_coe

deleted def measure_theory.simple_func'.const

deleted theorem measure_theory.simple_func'.const_apply

deleted theorem measure_theory.simple_func'.ext

deleted theorem measure_theory.simple_func'.is_measurable_cut

deleted def measure_theory.simple_func'.ite

deleted theorem measure_theory.simple_func'.ite_apply

deleted def measure_theory.simple_func'.itg

deleted theorem measure_theory.simple_func'.le_def

deleted def measure_theory.simple_func'.map

deleted theorem measure_theory.simple_func'.map_apply

deleted theorem measure_theory.simple_func'.map_itg

deleted theorem measure_theory.simple_func'.measurable

deleted theorem measure_theory.simple_func'.mem_range

deleted def measure_theory.simple_func'.pair

deleted theorem measure_theory.simple_func'.preimage_measurable

deleted def measure_theory.simple_func'.restrict

deleted theorem measure_theory.simple_func'.restrict_apply

deleted theorem measure_theory.simple_func'.restrict_preimage

deleted def measure_theory.simple_func'.seq

deleted theorem measure_theory.simple_func'.seq_itg

deleted theorem measure_theory.simple_func.add_congr

added theorem measure_theory.simple_func.add_eq_map₂

added theorem measure_theory.simple_func.add_integral

deleted theorem measure_theory.simple_func.add_sub_cancel_of_le

added def measure_theory.simple_func.approx

added theorem measure_theory.simple_func.approx_apply

added def measure_theory.simple_func.bind

added theorem measure_theory.simple_func.bind_apply

added theorem measure_theory.simple_func.bind_const

deleted theorem measure_theory.simple_func.coe_add

deleted theorem measure_theory.simple_func.coe_def

deleted theorem measure_theory.simple_func.coe_le_coe

added theorem measure_theory.simple_func.coe_map

added def measure_theory.simple_func.const

added theorem measure_theory.simple_func.const_apply

added theorem measure_theory.simple_func.const_mul_eq_map

added theorem measure_theory.simple_func.const_mul_integral

added def measure_theory.simple_func.eapprox

added def measure_theory.simple_func.ennreal_rat_embed

added theorem measure_theory.simple_func.ennreal_rat_embed_encode

deleted theorem measure_theory.simple_func.equiv_def

deleted theorem measure_theory.simple_func.equiv_iff

added theorem measure_theory.simple_func.ext

deleted theorem measure_theory.simple_func.finite_range

added theorem measure_theory.simple_func.finset_sup_apply

added def measure_theory.simple_func.integral

added theorem measure_theory.simple_func.integral_congr

added theorem measure_theory.simple_func.integral_le_integral

added theorem measure_theory.simple_func.integral_sup_le

added theorem measure_theory.simple_func.is_measurable_cut

added def measure_theory.simple_func.ite

added theorem measure_theory.simple_func.ite_apply

deleted def measure_theory.simple_func.itg'

deleted theorem measure_theory.simple_func.itg'_add

deleted theorem measure_theory.simple_func.itg'_eq_sum

deleted theorem measure_theory.simple_func.itg'_eq_sum_of_subset

deleted theorem measure_theory.simple_func.itg'_indicator

deleted theorem measure_theory.simple_func.itg'_mono

deleted theorem measure_theory.simple_func.itg'_zero

deleted def measure_theory.simple_func.itg

deleted theorem measure_theory.simple_func.itg_add

deleted theorem measure_theory.simple_func.itg_mono

deleted theorem measure_theory.simple_func.itg_zero

deleted theorem measure_theory.simple_func.le_antisymm

deleted theorem measure_theory.simple_func.le_antisymm_iff

deleted theorem measure_theory.simple_func.le_def

deleted theorem measure_theory.simple_func.le_iff_exists_add

deleted theorem measure_theory.simple_func.le_of_multiset_le

deleted def measure_theory.simple_func.lift₂

deleted theorem measure_theory.simple_func.lift₂_finite

deleted theorem measure_theory.simple_func.lift₂_is_measurable

deleted theorem measure_theory.simple_func.lift₂_val

added theorem measure_theory.simple_func.lintegral_eq_integral

added def measure_theory.simple_func.map

added theorem measure_theory.simple_func.map_apply

added theorem measure_theory.simple_func.map_integral

added theorem measure_theory.simple_func.map_map

modified theorem measure_theory.simple_func.measurable

added theorem measure_theory.simple_func.mem_range

added theorem measure_theory.simple_func.mem_restrict_range

added theorem measure_theory.simple_func.monotone_approx

added theorem measure_theory.simple_func.monotone_eapprox

added theorem measure_theory.simple_func.mul_apply

deleted def measure_theory.simple_func.of_fun

deleted theorem measure_theory.simple_func.of_fun_apply

deleted theorem measure_theory.simple_func.of_fun_val

added def measure_theory.simple_func.pair

added theorem measure_theory.simple_func.pair_apply

modified theorem measure_theory.simple_func.preimage_measurable

added theorem measure_theory.simple_func.range_const

added theorem measure_theory.simple_func.range_map

added def measure_theory.simple_func.restrict

added theorem measure_theory.simple_func.restrict_apply

added theorem measure_theory.simple_func.restrict_const_integral

added theorem measure_theory.simple_func.restrict_integral

added theorem measure_theory.simple_func.restrict_preimage'

added theorem measure_theory.simple_func.restrict_preimage

added def measure_theory.simple_func.seq

deleted theorem measure_theory.simple_func.sub_add_cancel_of_le

deleted theorem measure_theory.simple_func.sub_val

added theorem measure_theory.simple_func.sup_apply

added theorem measure_theory.simple_func.sup_eq_map₂

added theorem measure_theory.simple_func.supr_approx_apply

added theorem measure_theory.simple_func.supr_eapprox_apply

deleted def measure_theory.simple_func.to_fun

added theorem measure_theory.simple_func.zero_integral

deleted def measure_theory.simple_func

deleted theorem measure_theory.simple_itg_eq

deleted def measure_theory.upper_itg

deleted theorem measure_theory.upper_itg_add_le

deleted def measure_theory.upper_itg_def_subtype

deleted theorem measure_theory.upper_itg_simple

modified structure measure_theory.{u

added theorem supr_eq_of_tendsto

Modified analysis/measure_theory/measurable_space.lean

added theorem measurable_const

Modified analysis/measure_theory/measure_space.lean

added theorem measure_theory.volume_bUnion_finset

Modified data/finset.lean

added theorem finset.image_bind_filter_eq

added theorem finset.inf_eq_infi

added theorem finset.sup_eq_supr

Modified data/real/ennreal.lean

added theorem ennreal.coe_nat

added theorem ennreal.coe_to_nnreal_le_self

added theorem ennreal.le_of_forall_lt_one_mul_lt

added theorem ennreal.mul_inv_cancel

added theorem ennreal.mul_le_if_le_inv

added theorem ennreal.supr_coe_nat

Modified data/real/nnreal.lean

added theorem nnreal.le_of_forall_lt_one_mul_lt

added theorem nnreal.lt_inv_iff_mul_lt

added theorem nnreal.mul_le_if_le_inv

Modified data/set/basic.lean

added theorem set.compl_set_of

added theorem set.exists_range_iff

Modified order/complete_lattice.lean

added theorem lattice.Inf_eq_bot

modified theorem lattice.infi_eq_bot

added theorem lattice.supr_eq_bot

added theorem lattice.supr_eq_top

Modified order/filter.lean

added theorem filter.tendsto_at_top