Commit 2023-06-27 18:31 3f7a2eaf

View on Github →

feat(MeasureTheory): aesop rules for strong measurability + measurability? tactic (#5427) This PR adds aesop tags to a few lemmas pertaining to strong measurability, allowing to prove e.g. StronglyMeasurable Real.log using the measurability tactic. It also implements measurability? via aesop?.

Estimated changes

Modified Mathlib/MeasureTheory/Function/SpecialFunctions/Inner.lean

added theorem AEMeasurable.const_inner

added theorem AEMeasurable.inner_const

added theorem Measurable.const_inner

added theorem Measurable.inner_const

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

added theorem MeasureTheory.aefinStronglyMeasurable_of_aemeasurable

added theorem MeasureTheory.finStronglyMeasurable_of_measurable

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

Modified Mathlib/MeasureTheory/MeasurableSpace.lean

Modified Mathlib/MeasureTheory/MeasurableSpaceDef.lean

Modified Mathlib/Tactic/Measurability.lean

Modified test/measurability.lean