New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor(MeasureTheory): redefine ≤
on measures
#10714
Conversation
Redefine `≤` on `MeasureTheory.Measure` so that `μ ≤ ν ↔ ∀ s, μ s ≤ ν s` by definition instead of `∀ s, MeasurableSet s → μ s ≤ ν s`. The reasons are: - this way it is defeq to `≤` on outer measures; - if we decide to introduce an order on all `DFunLike` types **and** migrate measures to `FunLike`, then this is unavoidable; - the reasoning for the old definition was "it's slightly easier to prove `μ ≤ ν` this way"; the counter-argument is "it's slightly harder to apply `μ ≤ ν` this way". Other changes - golf some proofs broken by this change; - add `@[gcongr]` tags to some `ENNReal` lemmas; - fix the name `ENNReal.coe_lt_coe_of_le` -> `ENNReal.ENNReal.coe_lt_coe_of_lt`; - drop an unneeded `MeasurableSet` assumption in `set_lintegral_pdf_le_map`
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
Thanks!
bors merge
@@ -79,6 +79,7 @@ theorem toReal_le_toReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal ≤ b.toRe | |||
norm_cast | |||
#align ennreal.to_real_le_to_real ENNReal.toReal_le_toReal | |||
|
|||
@[gcongr] | |||
theorem toReal_mono (hb : b ≠ ∞) (h : a ≤ b) : a.toReal ≤ b.toReal := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
unrelated to this PR: we should move finiteness
to mathlib and add it as a gcongr
discharger.
Redefine `≤` on `MeasureTheory.Measure` so that `μ ≤ ν ↔ ∀ s, μ s ≤ ν s` by definition instead of `∀ s, MeasurableSet s → μ s ≤ ν s`. ### Reasons - this way it is defeq to `≤` on outer measures; - if we decide to introduce an order on all `DFunLike` types **and** migrate measures to `FunLike`, then this is unavoidable; - the reasoning for the old definition was "it's slightly easier to prove `μ ≤ ν` this way"; the counter-argument is "it's slightly harder to apply `μ ≤ ν` this way". ### Other changes - golf some proofs broken by this change; - add `@[gcongr]` tags to some `ENNReal` lemmas; - fix the name `ENNReal.coe_lt_coe_of_le` -> `ENNReal.ENNReal.coe_lt_coe_of_lt`; - drop an unneeded `MeasurableSet` assumption in `set_lintegral_pdf_le_map`
This PR was included in a batch that was canceled, it will be automatically retried |
Redefine `≤` on `MeasureTheory.Measure` so that `μ ≤ ν ↔ ∀ s, μ s ≤ ν s` by definition instead of `∀ s, MeasurableSet s → μ s ≤ ν s`. ### Reasons - this way it is defeq to `≤` on outer measures; - if we decide to introduce an order on all `DFunLike` types **and** migrate measures to `FunLike`, then this is unavoidable; - the reasoning for the old definition was "it's slightly easier to prove `μ ≤ ν` this way"; the counter-argument is "it's slightly harder to apply `μ ≤ ν` this way". ### Other changes - golf some proofs broken by this change; - add `@[gcongr]` tags to some `ENNReal` lemmas; - fix the name `ENNReal.coe_lt_coe_of_le` -> `ENNReal.ENNReal.coe_lt_coe_of_lt`; - drop an unneeded `MeasurableSet` assumption in `set_lintegral_pdf_le_map`
Pull request successfully merged into master. Build succeeded: |
≤
on measures≤
on measures
Redefine `≤` on `MeasureTheory.Measure` so that `μ ≤ ν ↔ ∀ s, μ s ≤ ν s` by definition instead of `∀ s, MeasurableSet s → μ s ≤ ν s`. ### Reasons - this way it is defeq to `≤` on outer measures; - if we decide to introduce an order on all `DFunLike` types **and** migrate measures to `FunLike`, then this is unavoidable; - the reasoning for the old definition was "it's slightly easier to prove `μ ≤ ν` this way"; the counter-argument is "it's slightly harder to apply `μ ≤ ν` this way". ### Other changes - golf some proofs broken by this change; - add `@[gcongr]` tags to some `ENNReal` lemmas; - fix the name `ENNReal.coe_lt_coe_of_le` -> `ENNReal.ENNReal.coe_lt_coe_of_lt`; - drop an unneeded `MeasurableSet` assumption in `set_lintegral_pdf_le_map`
Redefine `≤` on `MeasureTheory.Measure` so that `μ ≤ ν ↔ ∀ s, μ s ≤ ν s` by definition instead of `∀ s, MeasurableSet s → μ s ≤ ν s`. ### Reasons - this way it is defeq to `≤` on outer measures; - if we decide to introduce an order on all `DFunLike` types **and** migrate measures to `FunLike`, then this is unavoidable; - the reasoning for the old definition was "it's slightly easier to prove `μ ≤ ν` this way"; the counter-argument is "it's slightly harder to apply `μ ≤ ν` this way". ### Other changes - golf some proofs broken by this change; - add `@[gcongr]` tags to some `ENNReal` lemmas; - fix the name `ENNReal.coe_lt_coe_of_le` -> `ENNReal.ENNReal.coe_lt_coe_of_lt`; - drop an unneeded `MeasurableSet` assumption in `set_lintegral_pdf_le_map`
Redefine `≤` on `MeasureTheory.Measure` so that `μ ≤ ν ↔ ∀ s, μ s ≤ ν s` by definition instead of `∀ s, MeasurableSet s → μ s ≤ ν s`. ### Reasons - this way it is defeq to `≤` on outer measures; - if we decide to introduce an order on all `DFunLike` types **and** migrate measures to `FunLike`, then this is unavoidable; - the reasoning for the old definition was "it's slightly easier to prove `μ ≤ ν` this way"; the counter-argument is "it's slightly harder to apply `μ ≤ ν` this way". ### Other changes - golf some proofs broken by this change; - add `@[gcongr]` tags to some `ENNReal` lemmas; - fix the name `ENNReal.coe_lt_coe_of_le` -> `ENNReal.ENNReal.coe_lt_coe_of_lt`; - drop an unneeded `MeasurableSet` assumption in `set_lintegral_pdf_le_map`
Redefine `≤` on `MeasureTheory.Measure` so that `μ ≤ ν ↔ ∀ s, μ s ≤ ν s` by definition instead of `∀ s, MeasurableSet s → μ s ≤ ν s`. ### Reasons - this way it is defeq to `≤` on outer measures; - if we decide to introduce an order on all `DFunLike` types **and** migrate measures to `FunLike`, then this is unavoidable; - the reasoning for the old definition was "it's slightly easier to prove `μ ≤ ν` this way"; the counter-argument is "it's slightly harder to apply `μ ≤ ν` this way". ### Other changes - golf some proofs broken by this change; - add `@[gcongr]` tags to some `ENNReal` lemmas; - fix the name `ENNReal.coe_lt_coe_of_le` -> `ENNReal.ENNReal.coe_lt_coe_of_lt`; - drop an unneeded `MeasurableSet` assumption in `set_lintegral_pdf_le_map`
Redefine
≤
onMeasureTheory.Measure
so that
μ ≤ ν ↔ ∀ s, μ s ≤ ν s
by definitioninstead of
∀ s, MeasurableSet s → μ s ≤ ν s
.Reasons
≤
on outer measures;DFunLike
typesand migrate measures to
FunLike
, then this is unavoidable;"it's slightly easier to prove
μ ≤ ν
this way";the counter-argument is
"it's slightly harder to apply
μ ≤ ν
this way".Other changes
@[gcongr]
tags to someENNReal
lemmas;ENNReal.coe_lt_coe_of_le
->ENNReal.ENNReal.coe_lt_coe_of_lt
;MeasurableSet
assumptionin
set_lintegral_pdf_le_map