[Merged by Bors] - chore(measure_theory/*): make measurable_space arguments implicit, determined by the measure argument #8571
Conversation
If having two non-equal typeclass instances on the same type is going to be common, then this feels it is not an appropriate use of typeclasses in the first place. This PR looks like it makes things slightly less painful, but I think there's an underlying issue here worth thinking about more (as a follow-up). Usually the "multiple structures on the same type" problem is solved either with type aliases or replacing typeclasses with structures. It would be worth thinking about whether either of those approaches would work for probability theory. I have no objections to this PR, it just seems like a good excuse to draw attention to the underlying potential design issue |
|
Thanks for the comments, Eric. I agree that there is something worth thinking about more here. I did not want to change anything fundamental yet, since having measurable_space as a typeclass works very well for almost everything the the measure_theory folder. I limited my changes to the following well defined case: a lemma needs a measurable space and a measure, but works only if the measurable_space is the one used to define the measure. Then the change ensures that the measurable_space is given by the measure argument. |
RemyDegenne
added
awaiting-review
github-actions
bot
added
the
merge-conflict
|
This looks very very good to me. Can you merge master? |
github-actions
bot
removed
the
merge-conflict
There was a problem hiding this comment.
I like this a lot. This solves the issue of choosing the sigma-algebra in some situations, while not creating any real problem I can see. Of course, it won't solve all the issues (sometimes, we will still need to resort to @-versions), but in many cases this is a net improvement.
There are probably other situations where this strategy can be applied (see the comment on sigma-finite), but to avoid merge conflicts I wouldn't differ this one more than necessary. So I'd say, let's merge this now and improve later.
bors d+
| lemma integrable_of_forall_fin_meas_le' {μ : measure α'} (hm : m ≤ m0) | ||
| [@sigma_finite _ m (μ.trim hm)] (C : ℝ≥0∞) (hC : C < ∞) {f : α' → E} (hf_meas : ae_measurable f μ) | ||
| lemma integrable_of_forall_fin_meas_le' {μ : measure α} (hm : m ≤ m0) | ||
| [@sigma_finite _ m (μ.trim hm)] (C : ℝ≥0∞) (hC : C < ∞) {f : α → E} (hf_meas : ae_measurable f μ) |
There was a problem hiding this comment.
Just to be sure: couldn't also sigma_finite benefit from the same treatment as the other ones in this PR?
There was a problem hiding this comment.
It can also be changed. I forgot this one.
| @@ -643,7 +650,7 @@ if hf : injective f ∧ ∀ s, measurable_set s → measurable_set (f '' s) then | |||
| end | |||
| else 0 | |||
|
|
|||
| lemma comap_apply (f : α → β) (hfi : injective f) | |||
| lemma comap_apply {m0 : measurable_space α} (f : α → β) (hfi : injective f) | |||
There was a problem hiding this comment.
In this one, I don't see how m0 can be found by Lean. Did you want to put the structure on beta instead?
There was a problem hiding this comment.
Good catch. It should indeed be on beta. Thanks!
|
✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors r+ |
…termined 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 α)`.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
In the measure theory library, most of the definitions that depend on a measure have that form:
Suppose now that we have two
measurable_spacestructures onα:{m m0 : measurable_space α}and we have the measuresμ : measure α(which is a measure onm0) andμm : @measure α m. This will be common for probability theory applications. See for example theconditional_expectationfile.Then we can write
example_def μbut we cannot writeexample_def μmbecause themeasurable_spaceinferred ism0, which does not match the measurable space on whichμmis defined. We have to use@example_def _ m μminstead.This PR implements a simple fix: change
[measurable_space α] (μ : measure α)into{m : measurable_space α} (μ : measure α).Advantage: we can now use
example_def μmsince themeasurable_spaceargument is deduced from themeasureargument. This removes many@in all places wheremeasure.trimis used.Downsides:
(0 : measure α)instead of0in some lemmas.apply_instanceto findborel_spaceinstances.{m : measurable_space α} (μ : measure α)instead of simply(μ : measure α).