proof of L'Hopital rule #1371
proof of L'Hopital rule #1371
Conversation
| Hypothesis ab : a < b. | ||
| Hypotheses (cf : {within `[a, b], continuous f}) | ||
| (cg : {within `[a, b], continuous g}). | ||
| Hypotheses (fdf : forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) |
There was a problem hiding this comment.
Should we extend the predicate derivable_oo_continuous_bnd to include an option for an explicit derivative as an argument (E.G. derivable_oo_continuous_bnd_with f df x y)?
There was a problem hiding this comment.
Gave it a try, but couldn't extend quickly, so perhaps something to extend separately for a different PR?
There was a problem hiding this comment.
Yeah, I have no problem with that. Happy to deal with it later.
| Hypotheses (dg0 : forall x, x \in `]a, b[%R -> dg x != 0). | ||
|
|
||
| Lemma cauchy_MVT : | ||
| exists2 c, c \in `]a, b[%R & df c / dg c = (f b - f a) / (g b - g a). |
There was a problem hiding this comment.
Seems like callers will need to know that g b - g a != 0. We might as well deduplicate that a bit. I would recommend either an auxiliary lemma that for any g, a and b, {in ]a,b[, dg x != 0 -> g b - g a != 0. Or maybe put a g b - g a != 0 as an extra clause in the result of cauchy_MVT
There was a problem hiding this comment.
Done, as a separate lemma instead of inside the proof, but unsure if you perhaps meant outside of the MVT Cauchy section (so without all of its assumptions?)
Also I'm a bit unsure of what the naming convention would be for that one, so happy to rename it to something proper.
There was a problem hiding this comment.
This makes sense to me. I don't have any idea for naming here, so I'd say it's fine for now.
|
|
||
| Section lhopital. | ||
| Context {R : realType}. | ||
| Variables (f df g dg : R -> R) (a : R) (U : set R) (Ua : nbhs a U). |
There was a problem hiding this comment.
As usual, a question about boundary conditions. I'm a bit surprised to see we require f to be derivable in a full neighborhood of a. But then only take the right/left limit. Instead I would expect to see either a^'- U or a^'+U depending on the direction of the limit. Will the theorem still go through with that weakening?
There was a problem hiding this comment.
Good catch - I think this should go through, but changes are a bit more time-consuming than I expected so still in progress, should be done sometime next week.
Motivation for this change
Co-authored by: @affeldt-aist @hoheinzollern
Proofs of L'Hopital rule for limits taken on left and right, and Cauchy's mean value theorem.
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Reminder to reviewers