Commit 2021-08-12 07:03 cd2b5495

chore(measure_theory/*): make measurable_space arguments implicit, determined by the measure argument (#8571) In the measure theory library, most of the definitions that depend on a measure have that form:

def example_def {α} [measurable_space α] (μ : measure α) : some_type := sorry

Suppose now that we have two measurable_space structures on α : {m m0 : measurable_space α} and we have the measures μ : measure α (which is a measure on m0) and μm : @measure α m. This will be common for probability theory applications. See for example the conditional_expectation file. Then we can write example_def μ but we cannot write example_def μm because the measurable_space inferred is m0, which does not match the measurable space on which μm is defined. We have to use @example_def _ m μm instead. This PR implements a simple fix: change [measurable_space α] (μ : measure α) into {m : measurable_space α} (μ : measure α). Advantage: we can now use example_def μm since the measurable_space argument is deduced from the measure argument. This removes many @ in all places where measure.trim is used. Downsides:

• I have to write (0 : measure α) instead of 0 in some lemmas.
• I had to add two apply_instance to find borel_space instances.
• Whenever a lemma takes an explicit measure argument, we have to write {m : measurable_space α} (μ : measure α) instead of simply (μ : measure α).