feat(measure_theory/interval_integral): derivative of an integral#1944
feat(measure_theory/interval_integral): derivative of an integral#1944aceg00 wants to merge 20 commits intoleanprover-community:masterfrom
Conversation
| lemma indicator_eq_zero_ae (h : volume s = 0) : ∀ₘ a, indicator s f a = 0 := | ||
| begin | ||
| rw [all_ae_iff], | ||
| have : {a : α | ¬indicator s f a = 0} ⊆ s, |
There was a problem hiding this comment.
not_imp_comm.1 (λ h, indicator_of_not_mem h f)?
|
I think it would be easier to review if you split this into 3 PRs: (1) changes outside of |
|
BTW, do you need |
| end | ||
|
|
||
| lemma norm_integral_le_abs (a b : ℝ) (f : ℝ → β): | ||
| ∥(∫ x in a...b, f x)∥ ≤ abs (∫ x in a...b, ∥f x∥) := |
There was a problem hiding this comment.
Do you prove ∥(∫ x in a...b, f x)∥ ≤ ∫ x in a..b, ∥f x∥ as well (and equality of these RHSs)?
There was a problem hiding this comment.
It will be easier to prove trivial parts of some of these theorems if you have abs (∫ x in a...b, f x) = ∫ x in a..b, f x whenever f x ≥ 0 a.e. on a..b.
| (hgm : measurable_on a..b g) (hgi : integrable_on a..b g) : | ||
| abs (∫ x in a...b, f x) ≤ abs (∫ x in a...b, g x) := | ||
| begin | ||
| by_cases H : measurable_on a..b f ∧ integrable_on a..b f, |
There was a problem hiding this comment.
Probably not for this PR: does it make sense to deal with integrable but not measurable functions? If not, I propose to redefine integrable = measurable ∧ old_integrable.
| begin | ||
| by_cases H : measurable_on a..b f ∧ integrable_on a..b f, | ||
| { have H1 := H.1, have H2 := H.2, | ||
| split_ifs, |
There was a problem hiding this comment.
Please explicitly name the variable.
| { apply integral_on_le_integral_on_ae, assumption' }, | ||
| { filter_upwards [hf, hfg] λ a hf hfg h, le_trans (hf h) (hfg h) }, | ||
| { filter_upwards [hf] λ a hf, hf } }, | ||
| { simp only [interval_of_le' (le_of_not_ge h)] at *, |
There was a problem hiding this comment.
AFAIR, you have interval_of_not_ge
| refine integral_Icc_combine ba ac _ _ acm aci, | ||
| rwa [interval_swap], rwa [interval_swap] }, | ||
| { have := le_trans ac (le_of_not_ge bc), contradiction }, }, | ||
| show (∫ x in a...b, f x) + (∫ x in b...c, f x) = ∫ x in a...c, f x, |
There was a problem hiding this comment.
The rest of the proof should be either indented with 2 spaces or should be inside { ... }.
|
Another optional idea: if you use integrals over |
|
Thanks for the suggestion. I think I'll try to refactor using Currently singleton is not an issue, only three lines in |
|
@aceg00 Please tag me or replace |
|
@aceg00 what happened to this PR? Do you need help? It would be a really nice milestone to have this in mathlib. |
|
@aceg00 Are you going to come back to this PR? I really want to have it merged, so if you're not going to work on it in the next few weeks, I'd take over it. |
|
Is this still salvageable? The merge conflicts with |
This PR proves one of the fundamental theorems of calculus. I'll PR the other one after this one gets merged.
To help with the review, I made all commits meaningful. But perhaps this PR is still too big. If so, I'll split it.
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list