Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-09 11:29 b0c36dfd

View on Github →

feat(measure_theory/integration) lemmas for calculating integral of simple functions (#1659)

lemmas for calculating integration on simple functions
Updates
finsupp changed to fin_vol_supp
less conditions for to_real_mul_to_real
sum_lt_top with more abstraction
Fix extra arguments
One tactic per line

Estimated changes

Modified src/algebra/big_operators.lean

added theorem with_top.sum_lt_top

added theorem with_top.sum_lt_top_iff

Modified src/data/real/ennreal.lean

modified theorem ennreal.le_of_real_iff_to_real_le

modified theorem ennreal.of_real_eq_coe_nnreal

modified theorem ennreal.of_real_lt_iff_lt_to_real

added theorem ennreal.sum_lt_top

added theorem ennreal.sum_lt_top_iff

added theorem ennreal.to_nnreal_sum

added theorem ennreal.to_real_eq_to_real

added theorem ennreal.to_real_mul_to_real

added theorem ennreal.to_real_mul_top

modified theorem ennreal.to_real_of_real_mul

added theorem ennreal.to_real_sum

added theorem ennreal.to_real_top_mul

Modified src/measure_theory/integration.lean

added theorem measure_theory.lintegral_rw₁

added theorem measure_theory.lintegral_rw₂

modified theorem measure_theory.simple_func.approx_apply

modified theorem measure_theory.simple_func.approx_comp

modified theorem measure_theory.simple_func.ennreal_rat_embed_encode

added theorem measure_theory.simple_func.fin_vol_supp_map

added theorem measure_theory.simple_func.fin_vol_supp_of_fin_vol_supp_map

added theorem measure_theory.simple_func.fin_vol_supp_of_integral_lt_top

added theorem measure_theory.simple_func.fin_vol_supp_pair

added theorem measure_theory.simple_func.integral_lt_top_of_fin_vol_supp

modified theorem measure_theory.simple_func.integral_map

added theorem measure_theory.simple_func.integral_map_coe_lt_top

added theorem measure_theory.simple_func.lintegral_map

added theorem measure_theory.simple_func.map_preimage

added theorem measure_theory.simple_func.map_preimage_singleton

added theorem measure_theory.simple_func.pair_preimage

added theorem measure_theory.simple_func.pair_preimage_singleton

added theorem measure_theory.simple_func.preimage_eq_empty_iff

added theorem measure_theory.simple_func.smul_apply

added theorem measure_theory.simple_func.smul_eq_map

added theorem measure_theory.simple_func.volume_bUnion_preimage

Modified src/measure_theory/simple_func_dense.lean