Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-09 20:42 d9b91f3b

View on Github →

feat(measure_theory/tactic): add measurability tactic (#7756) Add a measurability tactic defined in the file measure_theory/tactic.lean, which is heavily inspired from the continuity tactic. It proves goals of the form measurable f, ae_measurable f µ and measurable_set s. Some tests are provided in tests/measurability.lean and the tactic was used to replace a few lines in integration.lean and mean_inequalities.lean.

Estimated changes

added theorem ae_measurable.div'
modified theorem ae_measurable.inv
added theorem ae_measurable.mul'
added theorem measurable.div'
modified theorem measurable.inv
added theorem measurable.mul'
modified theorem measurable_set_Icc
modified theorem measurable_set_Ici
modified theorem measurable_set_Ico
modified theorem measurable_set_Iic
modified theorem measurable_set_Iio
modified theorem measurable_set_Ioc
modified theorem measurable_set_Ioi
modified theorem measurable_set_Ioo
deleted theorem measurable.comp
modified theorem measurable.fst
modified theorem measurable.iterate
modified theorem measurable.prod
modified theorem measurable.snd
modified theorem measurable.subtype_coe
deleted def measurable
deleted theorem measurable_const
modified theorem measurable_from_nat
modified theorem measurable_fst
deleted theorem measurable_id
modified theorem measurable_inl
modified theorem measurable_inr
deleted theorem measurable_set.Inter
deleted theorem measurable_set.Inter_Prop
deleted theorem measurable_set.Union
deleted theorem measurable_set.Union_Prop
deleted theorem measurable_set.bInter
deleted theorem measurable_set.bUnion
deleted theorem measurable_set.compl
deleted theorem measurable_set.compl_iff
deleted theorem measurable_set.congr
deleted theorem measurable_set.const
deleted theorem measurable_set.diff
deleted theorem measurable_set.disjointed
deleted theorem measurable_set.empty
deleted theorem measurable_set.insert
deleted theorem measurable_set.inter
deleted theorem measurable_set.ite
deleted theorem measurable_set.of_compl
deleted theorem measurable_set.sInter
deleted theorem measurable_set.sUnion
deleted theorem measurable_set.union
deleted theorem measurable_set.univ
deleted def measurable_set
deleted theorem measurable_set_eq
deleted theorem measurable_set_insert
modified theorem measurable_set_mul_support
modified theorem measurable_snd
deleted theorem measurable_space.ext
deleted theorem measurable_space.ext_iff
deleted structure measurable_space
modified theorem measurable_subtype_coe
modified theorem measurable_swap
modified theorem measurable_unit
deleted theorem set.finite.measurable_set
modified theorem subsingleton.measurable
added theorem measurable.comp
added def measurable
added theorem measurable_const
added theorem measurable_id'
added theorem measurable_id
added theorem measurable_set.Inter
added theorem measurable_set.Union
added theorem measurable_set.bInter
added theorem measurable_set.bUnion
added theorem measurable_set.compl
added theorem measurable_set.congr
added theorem measurable_set.const
added theorem measurable_set.diff
added theorem measurable_set.empty
added theorem measurable_set.insert
added theorem measurable_set.inter
added theorem measurable_set.ite
added theorem measurable_set.sInter
added theorem measurable_set.sUnion
added theorem measurable_set.union
added theorem measurable_set.univ
added def measurable_set
added theorem measurable_set_eq
added theorem measurable_set_insert
added theorem measurable_space.ext
added structure measurable_space
deleted theorem ae_measurable.ae_eq_mk
deleted theorem ae_measurable.congr
deleted def ae_measurable.mk
deleted def ae_measurable
deleted theorem ae_measurable_congr
deleted theorem ae_measurable_const
modified theorem ae_measurable_zero_measure
deleted theorem measurable.ae_measurable
deleted theorem measure_theory.ae_all_iff
deleted theorem measure_theory.ae_eq_refl
deleted theorem measure_theory.ae_eq_set
deleted theorem measure_theory.ae_eq_symm
deleted theorem measure_theory.ae_iff
deleted theorem measure_theory.ae_imp_iff
deleted theorem measure_theory.ae_le_set
deleted theorem measure_theory.ae_of_all
deleted structure measure_theory.measure
deleted theorem measure_theory.mem_ae_iff
modified theorem subsingleton.ae_measurable
added theorem ae_measurable.ae_eq_mk
added theorem ae_measurable.congr
added def ae_measurable.mk
added def ae_measurable
added theorem ae_measurable_congr
added theorem ae_measurable_const
added theorem ae_measurable_id'
added theorem ae_measurable_id
added theorem measure_theory.ae_iff
added structure measure_theory.measure