-
Notifications
You must be signed in to change notification settings - Fork 299
[Merged by Bors] - feat(measure_theory): induction principles in measure theory #3978
Conversation
This looks very good to me and I was already able to put it to good use. But I'd like Sébastien to confirm these are the optimal statements since he knows this area much better. |
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.
This looks very good to me, I only have minor comments.
src/data/set/basic.lean
Outdated
@@ -922,6 +925,9 @@ ext $ assume x, ⟨assume ⟨hx, _⟩, hx, assume h, ⟨h, not_false⟩⟩ | |||
theorem diff_diff {u : set α} : s \ t \ u = s \ (t ∪ u) := | |||
ext $ by simp [not_or_distrib, and.comm, and.left_comm] | |||
|
|||
lemma diff_diff_comm {s t u : set α} : s \ t \ u = s \ u \ t := |
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.
I know parentheses are not necessary for Lean here, but could you add them for the human reader? (i.e., I don't know if you are talking about s \ (t \ u)
or (s \ t) \ u
without opening vscode)
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.
It's talking about the unique way that makes the lemma true in general :)
I added the parentheses.
src/measure_theory/integration.lean
Outdated
and supremum of increasing sequences of functions. -/ | ||
theorem measurable.ennreal_induction {α} [measurable_space α] {P : (α → ennreal) → Prop} | ||
(h_ind : ∀ (c : ennreal) ⦃s⦄, is_measurable s → P (indicator s (λ _, c))) | ||
(h_sum : ∀ ⦃f g⦄, measurable f → measurable g → P f → P g → P (f + g)) |
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.
sometimes, proving that a property is stable under sum is much easier when the functions have disjoint support. I think your induction principle still holds under this weaker assumption, right?
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.
It does. I was considering only adding it when I ever needed it, but I will add it now if you foresee that this will be useful.
I was a little hesitant, since there are many other conditions you can put on f
and g
(for example: f
is a simple function and g
is an indicator function with disjoint support and the intersection of their images is a subset of {0}
), and I'm not sure which of those will actually simplify arguments. I will also add a note to the docstring to that effect.
bors r+ |
This commit adds three induction principles for measure theory * To prove something for arbitrary simple functions * To prove something for arbitrary measurable functions into `ennreal` * To prove something for arbitrary measurable + integrable functions. This also adds some basic lemmas to various files. Not all of them are used in this PR, some will be used by near-future PRs. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Pull request successfully merged into master. Build succeeded: |
This commit adds three induction principles for measure theory * To prove something for arbitrary simple functions * To prove something for arbitrary measurable functions into `ennreal` * To prove something for arbitrary measurable + integrable functions. This also adds some basic lemmas to various files. Not all of them are used in this PR, some will be used by near-future PRs. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
This commit adds three induction principles for measure theory * To prove something for arbitrary simple functions * To prove something for arbitrary measurable functions into `ennreal` * To prove something for arbitrary measurable + integrable functions. This also adds some basic lemmas to various files. Not all of them are used in this PR, some will be used by near-future PRs. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
This commit adds three induction principles for measure theory
ennreal
This also adds some basic lemmas to various files. Not all of them are used in this PR, some will be used by near-future PRs.