Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-17 07:23 7d31f772

View on Github →

refactor(measure_theory/*): big refactor (#3373) Big refactor of integrals, fixes #3084 Make integral (f : α → E) (μ : measure α) the main definition, and use notation for other integrals (over a set and/or w.r.t. the canonical measure volume).

Estimated changes

Modified src/algebra/module.lean

added theorem linear_map.coe_injective

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_map.extend_unique

Modified src/data/indicator_function.lean

added theorem add_monoid_hom.map_indicator

added theorem set.indicator_le'

added theorem set.indicator_le

added theorem set.indicator_le_self'

added theorem set.indicator_le_self

Modified src/data/real/ennreal.lean

added theorem ennreal.coe_indicator

Modified src/data/real/nnreal.lean

added theorem nnreal.coe_indicator

Modified src/data/set/basic.lean

deleted theorem set.if_preimage

added theorem set.set_of_true

deleted theorem set.univ_def

Modified src/data/set/function.lean

added theorem set.piecewise_preimage

Modified src/measure_theory/ae_eq_fun.lean

deleted theorem measure_theory.ae_eq_fun.add_to_fun

deleted theorem measure_theory.ae_eq_fun.all_ae_mk_to_fun

added theorem measure_theory.ae_eq_fun.coe_fn_comp

added theorem measure_theory.ae_eq_fun.coe_fn_comp₂

added theorem measure_theory.ae_eq_fun.coe_fn_const

added theorem measure_theory.ae_eq_fun.coe_fn_edist

added theorem measure_theory.ae_eq_fun.coe_fn_inv

added theorem measure_theory.ae_eq_fun.coe_fn_le

added theorem measure_theory.ae_eq_fun.coe_fn_mk

added theorem measure_theory.ae_eq_fun.coe_fn_mul

added theorem measure_theory.ae_eq_fun.coe_fn_one

added theorem measure_theory.ae_eq_fun.coe_fn_pair

added theorem measure_theory.ae_eq_fun.coe_fn_pos_part

added theorem measure_theory.ae_eq_fun.coe_fn_smul

added theorem measure_theory.ae_eq_fun.coe_fn_sub

modified def measure_theory.ae_eq_fun.comp

deleted def measure_theory.ae_eq_fun.comp_edist

deleted theorem measure_theory.ae_eq_fun.comp_edist_self

deleted theorem measure_theory.ae_eq_fun.comp_edist_to_fun

added theorem measure_theory.ae_eq_fun.comp_eq_mk

deleted theorem measure_theory.ae_eq_fun.comp_eq_mk_to_fun

modified theorem measure_theory.ae_eq_fun.comp_mk

deleted theorem measure_theory.ae_eq_fun.comp_to_fun

added theorem measure_theory.ae_eq_fun.comp_to_germ

modified def measure_theory.ae_eq_fun.comp₂

added theorem measure_theory.ae_eq_fun.comp₂_eq_mk

deleted theorem measure_theory.ae_eq_fun.comp₂_eq_mk_to_fun

added theorem measure_theory.ae_eq_fun.comp₂_eq_pair

deleted theorem measure_theory.ae_eq_fun.comp₂_to_fun

added theorem measure_theory.ae_eq_fun.comp₂_to_germ

modified def measure_theory.ae_eq_fun.const

deleted theorem measure_theory.ae_eq_fun.const_to_fun

added theorem measure_theory.ae_eq_fun.edist_add_right

deleted theorem measure_theory.ae_eq_fun.edist_eq_add_add

added theorem measure_theory.ae_eq_fun.edist_eq_coe'

added theorem measure_theory.ae_eq_fun.edist_eq_coe

modified theorem measure_theory.ae_eq_fun.edist_mk_mk

modified theorem measure_theory.ae_eq_fun.edist_smul

deleted theorem measure_theory.ae_eq_fun.edist_to_fun'

deleted theorem measure_theory.ae_eq_fun.edist_to_fun

added theorem measure_theory.ae_eq_fun.edist_zero_eq_coe

deleted theorem measure_theory.ae_eq_fun.edist_zero_to_fun

deleted def measure_theory.ae_eq_fun.eintegral

deleted theorem measure_theory.ae_eq_fun.eintegral_add

deleted theorem measure_theory.ae_eq_fun.eintegral_eq_zero_iff

deleted theorem measure_theory.ae_eq_fun.eintegral_le_eintegral

deleted theorem measure_theory.ae_eq_fun.eintegral_mk

deleted theorem measure_theory.ae_eq_fun.eintegral_to_fun

deleted theorem measure_theory.ae_eq_fun.eintegral_zero

modified theorem measure_theory.ae_eq_fun.ext

added theorem measure_theory.ae_eq_fun.induction_on

added theorem measure_theory.ae_eq_fun.induction_on₂

added theorem measure_theory.ae_eq_fun.induction_on₃

added theorem measure_theory.ae_eq_fun.inv_mk

added theorem measure_theory.ae_eq_fun.inv_to_germ

deleted theorem measure_theory.ae_eq_fun.le_iff_to_fun_le

modified def measure_theory.ae_eq_fun.lift_pred

modified def measure_theory.ae_eq_fun.lift_rel

added theorem measure_theory.ae_eq_fun.lift_rel_iff_coe_fn

deleted theorem measure_theory.ae_eq_fun.lift_rel_iff_to_fun

modified theorem measure_theory.ae_eq_fun.lift_rel_mk_mk

added def measure_theory.ae_eq_fun.lintegral

added theorem measure_theory.ae_eq_fun.lintegral_add

added theorem measure_theory.ae_eq_fun.lintegral_coe_fn

added theorem measure_theory.ae_eq_fun.lintegral_eq_zero_iff

added theorem measure_theory.ae_eq_fun.lintegral_mk

added theorem measure_theory.ae_eq_fun.lintegral_mono

added theorem measure_theory.ae_eq_fun.lintegral_zero

modified def measure_theory.ae_eq_fun.mk

deleted theorem measure_theory.ae_eq_fun.mk_add_mk

added theorem measure_theory.ae_eq_fun.mk_coe_fn

modified theorem measure_theory.ae_eq_fun.mk_eq_mk

modified theorem measure_theory.ae_eq_fun.mk_le_mk

added theorem measure_theory.ae_eq_fun.mk_mul_mk

added theorem measure_theory.ae_eq_fun.mk_sub

deleted theorem measure_theory.ae_eq_fun.mk_sub_mk

added theorem measure_theory.ae_eq_fun.mk_to_germ

added theorem measure_theory.ae_eq_fun.mul_to_germ

deleted theorem measure_theory.ae_eq_fun.neg_mk

deleted theorem measure_theory.ae_eq_fun.neg_to_fun

modified theorem measure_theory.ae_eq_fun.one_def

deleted theorem measure_theory.ae_eq_fun.one_to_fun

added theorem measure_theory.ae_eq_fun.one_to_germ

added def measure_theory.ae_eq_fun.pair

added theorem measure_theory.ae_eq_fun.pair_eq_mk

added theorem measure_theory.ae_eq_fun.pair_mk_mk

modified def measure_theory.ae_eq_fun.pos_part

added theorem measure_theory.ae_eq_fun.pos_part_mk

deleted theorem measure_theory.ae_eq_fun.pos_part_to_fun

modified theorem measure_theory.ae_eq_fun.quot_mk_eq_mk

added theorem measure_theory.ae_eq_fun.quotient_out'_eq_coe_fn

deleted theorem measure_theory.ae_eq_fun.self_eq_mk

deleted theorem measure_theory.ae_eq_fun.smul_to_fun

added theorem measure_theory.ae_eq_fun.smul_to_germ

deleted theorem measure_theory.ae_eq_fun.sub_to_fun

added def measure_theory.ae_eq_fun.to_germ

added theorem measure_theory.ae_eq_fun.to_germ_eq

added theorem measure_theory.ae_eq_fun.to_germ_injective

deleted theorem measure_theory.ae_eq_fun.zero_def

deleted theorem measure_theory.ae_eq_fun.zero_to_fun

modified def measure_theory.ae_eq_fun

added def measure_theory.measure.ae_eq_setoid

Modified src/measure_theory/bochner_integration.lean

modified def measure_theory.integral

added theorem measure_theory.integral_add_meas

modified theorem measure_theory.integral_congr_ae

added theorem measure_theory.integral_const

modified theorem measure_theory.integral_div

modified theorem measure_theory.integral_eq

modified theorem measure_theory.integral_eq_lintegral_of_nonneg_ae

modified theorem measure_theory.integral_finset_sum

deleted theorem measure_theory.integral_le_integral

deleted theorem measure_theory.integral_le_integral_ae

added theorem measure_theory.integral_mono

modified theorem measure_theory.integral_mul_left

modified theorem measure_theory.integral_mul_right

modified theorem measure_theory.integral_neg

modified theorem measure_theory.integral_non_integrable

modified theorem measure_theory.integral_non_measurable

modified theorem measure_theory.integral_nonneg_of_ae

modified theorem measure_theory.integral_nonpos_of_nonpos_ae

modified theorem measure_theory.integral_smul

modified theorem measure_theory.integral_undef

modified theorem measure_theory.integral_zero

modified def measure_theory.l1.integral

modified theorem measure_theory.l1.integral_add

modified def measure_theory.l1.integral_clm

modified theorem measure_theory.l1.integral_eq

modified theorem measure_theory.l1.integral_eq_norm_pos_part_sub

modified theorem measure_theory.l1.integral_neg

modified theorem measure_theory.l1.integral_smul

modified theorem measure_theory.l1.integral_sub

modified theorem measure_theory.l1.integral_zero

modified theorem measure_theory.l1.norm_integral_le

modified theorem measure_theory.l1.simple_func.add_to_simple_func

modified theorem measure_theory.l1.simple_func.coe_add

added theorem measure_theory.l1.simple_func.coe_coe

modified theorem measure_theory.l1.simple_func.coe_neg

modified theorem measure_theory.l1.simple_func.coe_neg_part

modified theorem measure_theory.l1.simple_func.coe_pos_part

modified theorem measure_theory.l1.simple_func.coe_smul

modified theorem measure_theory.l1.simple_func.coe_sub

modified def measure_theory.l1.simple_func.coe_to_l1

modified theorem measure_theory.l1.simple_func.coe_zero

modified theorem measure_theory.l1.simple_func.dist_eq

modified theorem measure_theory.l1.simple_func.dist_to_simple_func

modified theorem measure_theory.l1.simple_func.edist_eq

deleted theorem measure_theory.l1.simple_func.exists_simple_func_near

modified def measure_theory.l1.simple_func.integral

modified theorem measure_theory.l1.simple_func.integral_add

modified def measure_theory.l1.simple_func.integral_clm

modified theorem measure_theory.l1.simple_func.integral_congr

deleted theorem measure_theory.l1.simple_func.integral_eq_bintegral

modified theorem measure_theory.l1.simple_func.integral_eq_integral

modified theorem measure_theory.l1.simple_func.integral_eq_lintegral

modified theorem measure_theory.l1.simple_func.integral_eq_norm_pos_part_sub

added theorem measure_theory.l1.simple_func.integral_l1_eq_integral

modified theorem measure_theory.l1.simple_func.integral_smul

modified theorem measure_theory.l1.simple_func.lintegral_edist_to_simple_func_lt_top

modified def measure_theory.l1.simple_func.neg_part

modified theorem measure_theory.l1.simple_func.neg_part_to_simple_func

modified theorem measure_theory.l1.simple_func.neg_to_simple_func

modified theorem measure_theory.l1.simple_func.norm_eq'

modified theorem measure_theory.l1.simple_func.norm_eq

deleted theorem measure_theory.l1.simple_func.norm_eq_bintegral

added theorem measure_theory.l1.simple_func.norm_eq_integral

modified theorem measure_theory.l1.simple_func.norm_integral_le_norm

modified theorem measure_theory.l1.simple_func.norm_of_simple_func

modified theorem measure_theory.l1.simple_func.norm_to_simple_func

modified def measure_theory.l1.simple_func.of_simple_func

modified theorem measure_theory.l1.simple_func.of_simple_func_add

modified theorem measure_theory.l1.simple_func.of_simple_func_eq_mk

modified theorem measure_theory.l1.simple_func.of_simple_func_eq_of_fun

modified theorem measure_theory.l1.simple_func.of_simple_func_neg

modified theorem measure_theory.l1.simple_func.of_simple_func_smul

modified theorem measure_theory.l1.simple_func.of_simple_func_sub

modified theorem measure_theory.l1.simple_func.of_simple_func_to_simple_func

modified theorem measure_theory.l1.simple_func.of_simple_func_zero

modified def measure_theory.l1.simple_func.pos_part

modified theorem measure_theory.l1.simple_func.pos_part_to_simple_func

modified theorem measure_theory.l1.simple_func.smul_to_simple_func

modified theorem measure_theory.l1.simple_func.sub_to_simple_func

modified def measure_theory.l1.simple_func.to_simple_func

modified theorem measure_theory.l1.simple_func.to_simple_func_eq_to_fun

modified theorem measure_theory.l1.simple_func.to_simple_func_of_simple_func

modified theorem measure_theory.l1.simple_func.zero_to_simple_func

modified def measure_theory.l1.simple_func

modified theorem measure_theory.norm_integral_le_integral_norm

modified theorem measure_theory.norm_integral_le_lintegral_norm

deleted def measure_theory.simple_func.bintegral

deleted theorem measure_theory.simple_func.bintegral_add

deleted theorem measure_theory.simple_func.bintegral_congr

deleted theorem measure_theory.simple_func.bintegral_eq_integral'

deleted theorem measure_theory.simple_func.bintegral_eq_integral

deleted theorem measure_theory.simple_func.bintegral_eq_lintegral'

deleted theorem measure_theory.simple_func.bintegral_eq_lintegral

deleted theorem measure_theory.simple_func.bintegral_neg

deleted theorem measure_theory.simple_func.bintegral_smul

deleted theorem measure_theory.simple_func.bintegral_sub

added theorem measure_theory.simple_func.fin_meas_supp.integrable

deleted theorem measure_theory.simple_func.fin_vol_supp_of_integrable

added theorem measure_theory.simple_func.integrable_iff_fin_meas_supp

deleted theorem measure_theory.simple_func.integrable_iff_fin_vol_supp

deleted theorem measure_theory.simple_func.integrable_iff_integral_lt_top

deleted theorem measure_theory.simple_func.integrable_of_fin_vol_supp

modified theorem measure_theory.simple_func.integrable_pair

added def measure_theory.simple_func.integral

added theorem measure_theory.simple_func.integral_add

added theorem measure_theory.simple_func.integral_add_meas

added theorem measure_theory.simple_func.integral_congr

added theorem measure_theory.simple_func.integral_eq_integral

added theorem measure_theory.simple_func.integral_eq_lintegral'

added theorem measure_theory.simple_func.integral_eq_lintegral

added theorem measure_theory.simple_func.integral_eq_sum_filter

added theorem measure_theory.simple_func.integral_neg

added theorem measure_theory.simple_func.integral_smul

added theorem measure_theory.simple_func.integral_sub

deleted theorem measure_theory.simple_func.map_bintegral

added theorem measure_theory.simple_func.map_integral

modified def measure_theory.simple_func.neg_part

deleted theorem measure_theory.simple_func.norm_bintegral_le_bintegral_norm

added theorem measure_theory.simple_func.norm_integral_le_integral_norm

modified def measure_theory.simple_func.pos_part

modified theorem measure_theory.tendsto_integral_of_dominated_convergence

added theorem measure_theory.tendsto_integral_of_l1

Modified src/measure_theory/borel_space.lean

deleted theorem is_measurable_eq

deleted theorem is_measurable_singleton

Modified src/measure_theory/category/Meas.lean

Modified src/measure_theory/giry_monad.lean

deleted theorem measure_theory.measure.integral_bind

deleted theorem measure_theory.measure.integral_join

added theorem measure_theory.measure.lintegral_bind

added theorem measure_theory.measure.lintegral_join

deleted theorem measure_theory.measure.measurable_integral

added theorem measure_theory.measure.measurable_lintegral

Modified src/measure_theory/indicator_function.lean

modified theorem indicator_congr_ae

modified theorem indicator_congr_of_set

modified theorem indicator_le_indicator_ae

Modified src/measure_theory/integration.lean

modified def measure_theory.lintegral

added theorem measure_theory.lintegral_Union

added theorem measure_theory.lintegral_Union_le

added theorem measure_theory.lintegral_add_meas

modified theorem measure_theory.lintegral_congr_ae

added theorem measure_theory.lintegral_const

modified theorem measure_theory.lintegral_const_mul_le

added theorem measure_theory.lintegral_dirac

modified theorem measure_theory.lintegral_eq_nnreal

deleted theorem measure_theory.lintegral_eq_supr_eapprox_integral

added theorem measure_theory.lintegral_eq_supr_eapprox_lintegral

added theorem measure_theory.lintegral_indicator

deleted theorem measure_theory.lintegral_le_lintegral_ae

added theorem measure_theory.lintegral_map

added theorem measure_theory.lintegral_mono'

modified theorem measure_theory.lintegral_mono

added theorem measure_theory.lintegral_mono_ae

modified theorem measure_theory.lintegral_rw₁

modified theorem measure_theory.lintegral_rw₂

added theorem measure_theory.lintegral_smul_meas

added theorem measure_theory.lintegral_sum_meas

deleted theorem measure_theory.lintegral_supr_const

modified theorem measure_theory.lintegral_zero

added theorem measure_theory.lintegral_zero_meas

added theorem measure_theory.meas_ge_le_lintegral_div

deleted def measure_theory.measure.integral

deleted theorem measure_theory.measure.integral_dirac

deleted theorem measure_theory.measure.integral_map

deleted theorem measure_theory.measure.integral_zero

modified def measure_theory.measure.with_density

deleted theorem measure_theory.measure.with_density_apply

modified theorem measure_theory.monotone_lintegral

added theorem measure_theory.mul_meas_ge_le_lintegral

deleted theorem measure_theory.mul_volume_ge_le_lintegral

deleted theorem measure_theory.simple_func.add_integral

added theorem measure_theory.simple_func.add_lintegral

added theorem measure_theory.simple_func.coe_add

added theorem measure_theory.simple_func.coe_const

added theorem measure_theory.simple_func.coe_injective

added theorem measure_theory.simple_func.coe_le

modified theorem measure_theory.simple_func.coe_map

added theorem measure_theory.simple_func.coe_mul

added theorem measure_theory.simple_func.coe_neg

added theorem measure_theory.simple_func.coe_piecewise

added theorem measure_theory.simple_func.coe_range

added theorem measure_theory.simple_func.coe_restrict

added theorem measure_theory.simple_func.coe_smul

added theorem measure_theory.simple_func.coe_sub

added theorem measure_theory.simple_func.coe_zero

modified theorem measure_theory.simple_func.const_apply

added theorem measure_theory.simple_func.const_lintegral

added theorem measure_theory.simple_func.const_lintegral_restrict

deleted theorem measure_theory.simple_func.const_mul_integral

added theorem measure_theory.simple_func.const_mul_lintegral

added theorem measure_theory.simple_func.const_zero

added theorem measure_theory.simple_func.eq_zero_of_mem_range_zero

added theorem measure_theory.simple_func.exists_range_iff

added theorem measure_theory.simple_func.fin_meas_supp.iff_lintegral_lt_top

added theorem measure_theory.simple_func.fin_meas_supp.lintegral_lt_top

added theorem measure_theory.simple_func.fin_meas_supp.map_iff

added theorem measure_theory.simple_func.fin_meas_supp.meas_preimage_singleton_ne_zero

added theorem measure_theory.simple_func.fin_meas_supp.of_lintegral_lt_top

added theorem measure_theory.simple_func.fin_meas_supp.of_map

added theorem measure_theory.simple_func.fin_meas_supp_iff

added theorem measure_theory.simple_func.fin_meas_supp_iff_support

deleted theorem measure_theory.simple_func.fin_vol_supp_map

deleted theorem measure_theory.simple_func.fin_vol_supp_of_fin_vol_supp_map

deleted theorem measure_theory.simple_func.fin_vol_supp_of_integral_lt_top

deleted theorem measure_theory.simple_func.fin_vol_supp_pair

added theorem measure_theory.simple_func.finite_range

added theorem measure_theory.simple_func.forall_range_iff

deleted def measure_theory.simple_func.integral

deleted theorem measure_theory.simple_func.integral_congr

deleted theorem measure_theory.simple_func.integral_le_integral

deleted theorem measure_theory.simple_func.integral_lt_top_of_fin_vol_supp

deleted theorem measure_theory.simple_func.integral_map

deleted theorem measure_theory.simple_func.integral_map_coe_lt_top

deleted theorem measure_theory.simple_func.integral_sup_le

modified theorem measure_theory.simple_func.is_measurable_cut

added theorem measure_theory.simple_func.is_measurable_fiber

added theorem measure_theory.simple_func.is_measurable_preimage

deleted def measure_theory.simple_func.ite

deleted theorem measure_theory.simple_func.ite_apply

added theorem measure_theory.simple_func.le_sup_lintegral

added def measure_theory.simple_func.lintegral

added theorem measure_theory.simple_func.lintegral_add

added theorem measure_theory.simple_func.lintegral_congr

deleted theorem measure_theory.simple_func.lintegral_eq_integral

added theorem measure_theory.simple_func.lintegral_eq_lintegral

added theorem measure_theory.simple_func.lintegral_eq_of_measure_preimage

added theorem measure_theory.simple_func.lintegral_eq_of_subset

modified theorem measure_theory.simple_func.lintegral_map

added theorem measure_theory.simple_func.lintegral_mono

added theorem measure_theory.simple_func.lintegral_restrict

added theorem measure_theory.simple_func.lintegral_smul

added theorem measure_theory.simple_func.lintegral_sum

added theorem measure_theory.simple_func.lintegral_zero

added def measure_theory.simple_func.lintegralₗ

modified theorem measure_theory.simple_func.map_apply

added theorem measure_theory.simple_func.map_coe_ennreal_restrict

added theorem measure_theory.simple_func.map_coe_nnreal_restrict

added theorem measure_theory.simple_func.map_const

deleted theorem measure_theory.simple_func.map_integral

added theorem measure_theory.simple_func.map_lintegral

added theorem measure_theory.simple_func.map_restrict_of_zero

added theorem measure_theory.simple_func.mem_image_of_mem_range_restrict

modified theorem measure_theory.simple_func.mem_range

added theorem measure_theory.simple_func.mem_range_of_measure_ne_zero

added theorem measure_theory.simple_func.mem_range_self

modified theorem measure_theory.simple_func.mem_restrict_range

modified theorem measure_theory.simple_func.mul_apply

added theorem measure_theory.simple_func.mul_eq_map₂

added def measure_theory.simple_func.piecewise

added theorem measure_theory.simple_func.piecewise_apply

added theorem measure_theory.simple_func.piecewise_compl

added theorem measure_theory.simple_func.piecewise_empty

added theorem measure_theory.simple_func.piecewise_univ

deleted theorem measure_theory.simple_func.preimage_measurable

modified theorem measure_theory.simple_func.range_const

added theorem measure_theory.simple_func.range_zero

modified def measure_theory.simple_func.restrict

modified theorem measure_theory.simple_func.restrict_apply

deleted theorem measure_theory.simple_func.restrict_const_integral

added theorem measure_theory.simple_func.restrict_const_lintegral

added theorem measure_theory.simple_func.restrict_empty

deleted theorem measure_theory.simple_func.restrict_integral

added theorem measure_theory.simple_func.restrict_lintegral

added theorem measure_theory.simple_func.restrict_lintegral_eq_lintegral_restrict

added theorem measure_theory.simple_func.restrict_mono

added theorem measure_theory.simple_func.restrict_of_not_measurable

deleted theorem measure_theory.simple_func.restrict_preimage'

modified theorem measure_theory.simple_func.restrict_preimage

added theorem measure_theory.simple_func.restrict_preimage_singleton

added theorem measure_theory.simple_func.restrict_univ

modified theorem measure_theory.simple_func.smul_eq_map

modified theorem measure_theory.simple_func.sup_apply

added theorem measure_theory.simple_func.support_eq

modified theorem measure_theory.simple_func.supr_eapprox_apply

deleted theorem measure_theory.simple_func.volume_bUnion_preimage

deleted theorem measure_theory.simple_func.zero_integral

added theorem measure_theory.simple_func.zero_lintegral

deleted theorem measure_theory.volume_ge_le_lintegral_div

added theorem measure_theory.with_density_apply

Modified src/measure_theory/l1_space.lean

modified theorem measure_theory.ae_eq_fun.integrable.add

modified theorem measure_theory.ae_eq_fun.integrable.neg

modified theorem measure_theory.ae_eq_fun.integrable.smul

modified theorem measure_theory.ae_eq_fun.integrable.sub

modified def measure_theory.ae_eq_fun.integrable

added theorem measure_theory.ae_eq_fun.integrable_coe_fn

deleted theorem measure_theory.ae_eq_fun.integrable_to_fun

modified theorem measure_theory.ae_eq_fun.integrable_zero

modified theorem measure_theory.all_ae_of_real_F_le_bound

modified theorem measure_theory.all_ae_of_real_f_le_bound

modified theorem measure_theory.all_ae_tendsto_of_real_norm

added theorem measure_theory.integrable.add_meas

added theorem measure_theory.integrable.congr

added theorem measure_theory.integrable.left_of_add_meas

modified theorem measure_theory.integrable.max_zero

modified theorem measure_theory.integrable.min_zero

added theorem measure_theory.integrable.mono

added theorem measure_theory.integrable.mono_meas

added theorem measure_theory.integrable.mono_set

modified theorem measure_theory.integrable.neg

modified theorem measure_theory.integrable.norm

added theorem measure_theory.integrable.right_of_add_meas

modified theorem measure_theory.integrable.smul

added theorem measure_theory.integrable.smul_meas

added theorem measure_theory.integrable.union

modified def measure_theory.integrable

added theorem measure_theory.integrable_congr

deleted theorem measure_theory.integrable_congr_ae

added theorem measure_theory.integrable_const

modified theorem measure_theory.integrable_iff_edist

modified theorem measure_theory.integrable_iff_norm

modified theorem measure_theory.integrable_iff_of_real

modified theorem measure_theory.integrable_neg_iff

modified theorem measure_theory.integrable_norm_iff

deleted theorem measure_theory.integrable_of_ae_eq

modified theorem measure_theory.integrable_of_integrable_bound

deleted theorem measure_theory.integrable_of_le

deleted theorem measure_theory.integrable_of_le_ae

modified theorem measure_theory.integrable_zero

modified theorem measure_theory.l1.add_to_fun

modified theorem measure_theory.l1.coe_add

added theorem measure_theory.l1.coe_coe

modified theorem measure_theory.l1.coe_neg

modified theorem measure_theory.l1.coe_pos_part

modified theorem measure_theory.l1.coe_smul

modified theorem measure_theory.l1.coe_sub

modified theorem measure_theory.l1.coe_zero

modified theorem measure_theory.l1.continuous_neg_part

modified theorem measure_theory.l1.continuous_pos_part

modified theorem measure_theory.l1.dist_eq

modified theorem measure_theory.l1.dist_to_fun

modified theorem measure_theory.l1.edist_eq

modified theorem measure_theory.l1.lintegral_edist_to_fun_lt_top

modified theorem measure_theory.l1.mk_to_fun

modified def measure_theory.l1.neg_part

modified theorem measure_theory.l1.neg_part_to_fun_eq_max

modified theorem measure_theory.l1.neg_part_to_fun_eq_min

modified theorem measure_theory.l1.neg_to_fun

modified theorem measure_theory.l1.norm_eq

modified theorem measure_theory.l1.norm_eq_nnnorm_to_fun

modified theorem measure_theory.l1.norm_eq_norm_to_fun

modified theorem measure_theory.l1.norm_le_norm_of_ae_le

modified def measure_theory.l1.of_fun

modified theorem measure_theory.l1.of_fun_eq_mk

modified theorem measure_theory.l1.of_fun_smul

modified theorem measure_theory.l1.of_fun_to_fun

modified def measure_theory.l1.pos_part

modified theorem measure_theory.l1.pos_part_to_fun

modified theorem measure_theory.l1.smul_to_fun

modified theorem measure_theory.l1.sub_to_fun

modified theorem measure_theory.l1.to_fun_of_fun

modified theorem measure_theory.l1.zero_to_fun

modified def measure_theory.l1

modified theorem measure_theory.lintegral_nnnorm_zero

Modified src/measure_theory/measurable_space.lean

modified theorem is_measurable.compl_iff

modified theorem is_measurable.empty

added theorem is_measurable.inl_image

added theorem is_measurable.insert

added theorem is_measurable.subtype_image

modified theorem is_measurable.univ

added theorem is_measurable_eq

deleted theorem is_measurable_inl_image

added theorem is_measurable_insert

deleted theorem is_measurable_subtype_image

deleted theorem measurable.if

added theorem measurable.indicator

added theorem measurable.piecewise

deleted theorem measurable.preimage

added theorem measurable.sum_rec

modified def measurable

modified theorem measurable_const

added theorem measurable_fst

modified theorem measurable_id

added theorem measurable_iff_comap_le

added theorem measurable_iff_le_map

modified theorem measurable_inl

modified theorem measurable_inr

added theorem measurable_one

added theorem measurable_snd

added theorem measurable_subtype_coe

deleted theorem measurable_sum_rec

deleted theorem measurable_zero

added theorem set.finite.is_measurable

Modified src/measure_theory/measure_space.lean

modified theorem measure_theory.ae_eq_refl

modified theorem measure_theory.ae_eq_symm

modified theorem measure_theory.ae_eq_trans

modified theorem measure_theory.ae_iff

added theorem measure_theory.ae_map_iff

modified theorem measure_theory.ae_of_all

added theorem measure_theory.ae_restrict_eq

added theorem measure_theory.coe_to_outer_measure

added theorem measure_theory.dirac_ae_eq

added theorem measure_theory.eventually_dirac

added theorem measure_theory.eventually_eq_dirac'

added theorem measure_theory.eventually_eq_dirac

added theorem measure_theory.exists_is_measurable_superset_iff_measure_eq_zero

added theorem measure_theory.le_to_measure_apply

modified theorem measure_theory.measure.add_apply

added theorem measure_theory.measure.coe_add

added theorem measure_theory.measure.coe_smul

added theorem measure_theory.measure.coe_zero

added def measure_theory.measure.cofinite

added def measure_theory.measure.comap

added theorem measure_theory.measure.comap_apply

added theorem measure_theory.measure.count_apply

added theorem measure_theory.measure.count_apply_finset

added theorem measure_theory.measure.dirac_apply'

added theorem measure_theory.measure.dirac_apply_of_mem

added theorem measure_theory.measure.eq_zero_of_not_nonempty

added theorem measure_theory.measure.eventually_cofinite

modified theorem measure_theory.measure.ext

added theorem measure_theory.measure.le_lift_linear_apply

added theorem measure_theory.measure.le_restrict_apply

added def measure_theory.measure.lift_linear

added theorem measure_theory.measure.lift_linear_apply

added theorem measure_theory.measure.lt_iff'

added theorem measure_theory.measure.lt_iff

modified def measure_theory.measure.map

modified theorem measure_theory.measure.map_apply

added theorem measure_theory.measure.map_comap_subtype_coe

added theorem measure_theory.measure.mem_cofinite

added def measure_theory.measure.restrict

added theorem measure_theory.measure.restrict_Union

added theorem measure_theory.measure.restrict_Union_apply

added theorem measure_theory.measure.restrict_Union_le

added theorem measure_theory.measure.restrict_add

added theorem measure_theory.measure.restrict_apply

added theorem measure_theory.measure.restrict_apply_eq_zero'

added theorem measure_theory.measure.restrict_apply_eq_zero

added theorem measure_theory.measure.restrict_empty

added theorem measure_theory.measure.restrict_mono

added theorem measure_theory.measure.restrict_smul

added theorem measure_theory.measure.restrict_sum

added theorem measure_theory.measure.restrict_union

added theorem measure_theory.measure.restrict_union_apply

added theorem measure_theory.measure.restrict_union_le

added theorem measure_theory.measure.restrict_univ

added theorem measure_theory.measure.restrict_zero

added def measure_theory.measure.restrictₗ

added theorem measure_theory.measure.restrictₗ_apply

deleted theorem measure_theory.measure.smul_apply

added theorem measure_theory.measure.smul_to_outer_measure

added theorem measure_theory.measure.sum_apply

added theorem measure_theory.measure.sum_bool

added theorem measure_theory.measure.to_outer_measure_injective

deleted theorem measure_theory.measure.zero_apply

modified theorem measure_theory.measure.zero_to_outer_measure

added theorem measure_theory.measure_bUnion_finset_le

added theorem measure_theory.measure_bUnion_le

added theorem measure_theory.measure_congr

added theorem measure_theory.measure_diff_of_ae_imp

added theorem measure_theory.measure_le_of_ae_imp

modified theorem measure_theory.measure_zero_iff_ae_nmem

modified theorem measure_theory.mem_ae_iff

added theorem measure_theory.mem_ae_map_iff

added theorem measure_theory.mem_dirac_ae_iff

added theorem measure_theory.nonempty_of_measure_ne_zero

modified theorem measure_theory.outer_measure.trim_eq_infi'

modified theorem measure_theory.outer_measure.trim_smul

added theorem measure_theory.sum_measure_preimage_singleton

modified theorem measure_theory.to_measure_to_outer_measure

modified theorem measure_theory.to_outer_measure_apply

modified theorem measure_theory.to_outer_measure_to_measure

added theorem measure_theory.tsum_measure_preimage_singleton

Modified src/measure_theory/outer_measure.lean

modified theorem measure_theory.outer_measure.add_apply

added theorem measure_theory.outer_measure.coe_add

added theorem measure_theory.outer_measure.coe_fn_injective

added theorem measure_theory.outer_measure.coe_smul

added theorem measure_theory.outer_measure.coe_zero

added def measure_theory.outer_measure.comap

added theorem measure_theory.outer_measure.comap_apply

modified theorem measure_theory.outer_measure.ext

modified def measure_theory.outer_measure.map

modified theorem measure_theory.outer_measure.measure_of_eq_coe

added def measure_theory.outer_measure.restrict

added theorem measure_theory.outer_measure.restrict_apply

modified theorem measure_theory.outer_measure.smul_apply

deleted theorem measure_theory.outer_measure.zero_apply

Modified src/measure_theory/set_integral.lean

deleted theorem integrable_on.add

deleted theorem integrable_on.divide

deleted theorem integrable_on.mul_left

deleted theorem integrable_on.mul_right

deleted theorem integrable_on.neg

deleted theorem integrable_on.smul

deleted theorem integrable_on.sub

deleted theorem integrable_on.subset

deleted theorem integrable_on.union

deleted def integrable_on

deleted theorem integrable_on_congr

deleted theorem integrable_on_congr_ae

deleted theorem integrable_on_empty

deleted theorem integrable_on_norm_iff

deleted theorem integral_on_Union

deleted theorem integral_on_add

deleted theorem integral_on_congr

deleted theorem integral_on_congr_of_ae_eq

deleted theorem integral_on_congr_of_set

deleted theorem integral_on_div

deleted theorem integral_on_le_integral_on

deleted theorem integral_on_le_integral_on_ae

deleted theorem integral_on_mul_left

deleted theorem integral_on_mul_right

deleted theorem integral_on_neg

deleted theorem integral_on_non_integrable

deleted theorem integral_on_non_measurable

deleted theorem integral_on_nonneg

deleted theorem integral_on_nonneg_of_ae

deleted theorem integral_on_nonpos

deleted theorem integral_on_nonpos_of_ae

deleted theorem integral_on_smul

deleted theorem integral_on_sub

deleted theorem integral_on_undef

deleted theorem integral_on_union

deleted theorem integral_on_union_ae

deleted theorem integral_on_zero

deleted theorem is_measurable.inter_preimage

deleted theorem measurable.measurable_on

deleted theorem measurable.measurable_on_univ

deleted theorem measurable_on.subset

deleted theorem measurable_on.union

deleted def measurable_on

deleted theorem measurable_on_empty

deleted theorem measurable_on_singleton

deleted theorem measure_theory.integrable.integrable_on

deleted theorem tendsto_integral_on_of_antimono

deleted theorem tendsto_integral_on_of_monotone

Modified src/measure_theory/simple_func_dense.lean

modified theorem measure_theory.simple_func_sequence_tendsto'

Modified src/order/complete_lattice.lean

modified theorem infi_eq_bot

Modified src/order/filter/basic.lean

added theorem filter.eventually_eq.prod_mk

added theorem filter.eventually_inf_principal

modified theorem filter.mem_inf_principal

Modified src/order/filter/germ.lean

added theorem filter.germ.map₂_coe

Modified src/topology/algebra/infinite_sum.lean

added theorem tsum_subtype

Modified src/topology/algebra/module.lean

added theorem continuous_linear_map.coe_injective'

added theorem continuous_linear_map.coe_injective

added theorem continuous_linear_map.coe_mk'

added theorem continuous_linear_map.coe_mk

Modified src/topology/algebra/uniform_ring.lean

Modified src/topology/continuous_on.lean

Modified src/topology/dense_embedding.lean

deleted theorem dense_inducing.extend_e_eq

modified theorem dense_inducing.extend_eq

added theorem dense_inducing.extend_eq_at

deleted theorem dense_inducing.extend_eq_of_cont

added theorem dense_inducing.extend_eq_of_tendsto

added theorem dense_inducing.extend_unique

added theorem dense_inducing.extend_unique_at

Modified src/topology/stone_cech.lean

Modified src/topology/uniform_space/abstract_completion.lean

Modified src/topology/uniform_space/uniform_embedding.lean

added theorem uniformly_extend_unique