[Merged by Bors] - feat(analysis/complex/basic): add several trivial lemmas for differentiable functions. #8418
Conversation
justadzr
added
RFC
src/analysis/complex/basic.lean
Outdated
|
|
||
| variables {f : ℂ → ℂ} {z : ℂ} | ||
|
|
||
| lemma fderiv_eq_fderiv_of_holomorph (h : differentiable_at ℂ f z) : |
There was a problem hiding this comment.
I don't know the conventions... have we established to write of_holomorph for complex differentiable functions?
src/analysis/complex/basic.lean
Outdated
| by { rw (h.restrict_scalars ℝ).has_fderiv_at.unique (h.has_fderiv_at.restrict_scalars ℝ), | ||
| simp only [coe_restrict_scalars'], } | ||
|
|
||
| lemma has_fderiv_at_of_eq {f' : ℂ →L[ℝ] ℂ} {g' : ℂ →L[ℂ] ℂ} |
There was a problem hiding this comment.
Can this be generalized away from the reals and complexes? I can imagine this might be useful for other extensions of complete normed fields (or whatever assumptions are needed to get fderiv working).
There was a problem hiding this comment.
I think generalizing these lemmas (fderiv_eq_fderiv_of_holomorph and has_fderiv_at_of_eq) would be really nice.
There was a problem hiding this comment.
It seems that I can also generalize the lemma holomorphic_iff_is_complex_linear (the old is_complex_linear_iff_holomorph) to differentiable_iff_is_linear_map, but I am not sure if that's something useful for other fields.
jcommelin
added
awaiting-author
justadzr
added
awaiting-review
|
There's a general shift away from unbundled statements (eg, |
justadzr
changed the title
There was a problem hiding this comment.
Thanks! These lemmas are hard to name, but I think an important point is that all of them should have restrict_scalars in the name somewhere.
Maybe has_fderiv_within_at_of_restrict_scalars instead of has_fderiv_within_at_of_eq, and differentiable_within_at_iff_restrict_scalars instead of differentiable_within_at_iff_exists_linear_map? (Unfortunately these names are still a bit misleading.) Or let me know if you have other ideas.
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
Done! |
|
✌️ justadzr can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
the
delegated
github-actions
bot
removed
the
awaiting-review
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
|
bors r+ |
…tiable functions. (#8418) This file relates the differentiability of a function to the linearity of its `fderiv`. Co-authored-by: justadzr <66561890+justadzr@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This file relates the differentiability of a function to the linearity of its
fderiv.Hello, some of the lemmas are quite trivial but are mentioned/used previously in other PRs or branches. I am not sure if analysis/complex/basic is the right place to put these lemmas, but it seems to me that similar lemmas were put in this particular file in the branch "complex-diff".