[Merged by Bors] - feat(measure_theory/interval_integral): more versions of FTC-1#3709
[Merged by Bors] - feat(measure_theory/interval_integral): more versions of FTC-1#3709
Conversation
|
While adding docs I found some holes in API. I'll work on this tonight or tomorrow. |
Should this be mentioned in a module doc string? |
sgouezel
left a comment
There was a problem hiding this comment.
This is very nice: the formulations of the different versions of the FTC are really neat, and you have been able to factor out the proof part very efficiently. Thanks!
| the difference $F_μ(b)-F_μ(a)$, where $F_μ(a)=μ(-∞, a]$ is the | ||
| [cumulative distribution function](https://en.wikipedia.org/wiki/Cumulative_distribution_function) | ||
| of `μ`. | ||
|
|
There was a problem hiding this comment.
Could you add comments on the different versions of the FTC you prove, in the file-level docstring?
Now `interval_integral` has `#exit` and many outdated docstrings.
|
While working on the docs I've realized that I have no |
Lemmas from FTC-1 (`has_strict_deriv`) #3709
|
I rewrote large parts of this PR to add differentiability in both endpoints. |
sgouezel
left a comment
There was a problem hiding this comment.
Thanks! In addition to minor comments, my main concern is that the file-level docstring could (should?) be exanded a lot, both in the statements section (can you explain what you prove, maybe not all versions but at least one or two relevant versions), and also in the implementation section (comment on the specific type classes you introduce, and how they are used and how they make it possible to avoid proof duplication).
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…thlib into FTC-strict
|
@sgouezel I tried to address all your comments. |
|
bors r+ Thanks! |
Left/right derivative, strict derivative, differentiability in both endpoints. Other changes: * rename `filter.tendsto_le_left` and `filter.tendsto_le_right` to `filter.tendsto.mono_left` and `filter.tendsto.mono_right`, swap arguments; * rename `order_top.tendsto_at_top` to `order_top.tendsto_at_top_nhds`; * introduce `tendsto_Ixx_class` instead of `is_interval_generated`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
|
Pull request successfully merged into master. Build succeeded: |
Left/right derivative, strict derivative, differentiability in both endpoints.
Other changes:
filter.tendsto_le_leftandfilter.tendsto_le_righttofilter.tendsto.mono_leftandfilter.tendsto.mono_right, swap arguments;order_top.tendsto_at_toptoorder_top.tendsto_at_top_nhds;tendsto_Ixx_classinstead ofis_interval_generated.Some lemmas assume
(l : filter α) [is_interval_generated l] (_ : pure b ≤ l) (l ≤ 𝓝 b).This is a fancy way to say “
lis one ofpure b,𝓝[Iic b] b,𝓝[Ici b] b,𝓝 b”in order to prove a lemma for the three non-trivial cases simultaneously.