feat(analysis/complex/basic): restriction of scalars, real differentiability of complex functions#1716
Conversation
jcommelin
left a comment
There was a problem hiding this comment.
Nice work! At some point we'll have to do the adjunction between restriction of scalars and tensor product as well. (With and/or without category_theory/...)
Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>
Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>
robertylewis
left a comment
There was a problem hiding this comment.
This looks basically ready to me -- unless some of the analysis people (@avigad ?) want to weigh in, I'd say it's almost good to go.
| has_fderiv_within_at f f' s x ↔ has_deriv_within_at f (f' 1) s x := | ||
| by simp [has_deriv_within_at, has_deriv_at_filter, has_fderiv_within_at] | ||
|
|
||
| lemma has_deriv_within_at_iff_has_fderiv_within_at {f' : F} : |
There was a problem hiding this comment.
The existing iff lemmas around here seem to go in the other direction -- fderiv on the left, deriv on the right. Is there a reason this one goes the other way? Naively, the LHS looks simpler to me.
There was a problem hiding this comment.
All these lemmas will most of the time be used from left to right, in the following way: you have a simple expression, but you may want to transform it into something more complicated to which you will apply an existing theorem. The other direction is essentially not used, as there is no reason why you would stumble on something of this specific form in a proof. This is why all these lemmas are written with the simple expression on the left, and without a simp attribute.
There was a problem hiding this comment.
I see. I think the naming is a little confusing -- it sounds like the symmetric version of the lemma right before. But I don't have a better suggestion. Maybe it would help to have doc strings on both directions that explain the difference? It would show up if someone tried to use one when they needed the other.
In any case, I don't think it's a very big deal.
There was a problem hiding this comment.
I have added docstrings, hopefully they clarify things at least a little bit.
…ability of complex functions (leanprover-community#1716) * restrict scalar * staging * complete proof * staging * cleanup * staging * cleanup * docstring * docstring * reviewer's comments * Update src/analysis/complex/basic.lean Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com> * Update src/analysis/calculus/fderiv.lean Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com> * add ! in docstrings [ci skip] * more doc formatting in fderiv * fix comments * add docstrings
…ability of complex functions (leanprover-community#1716) * restrict scalar * staging * complete proof * staging * cleanup * staging * cleanup * docstring * docstring * reviewer's comments * Update src/analysis/complex/basic.lean Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com> * Update src/analysis/calculus/fderiv.lean Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com> * add ! in docstrings [ci skip] * more doc formatting in fderiv * fix comments * add docstrings
…st year; I presume the real code goes back to leanprover-community/mathlib3#1716 in 2019.
…diff-a959c7a7d6b5f608638e708fc07590f8a8e1f7b86f05cd9296b0bf3574f86760; which moved content from analysis/complex/basic... which also goes back to 2019 (e.g. the lemma has_deriv_at.real_of_complex was added in leanprover-community/mathlib3#1716.
The goal of this PR is to prove the following theorem
(designed for the differentiability over real numbers of exponential, sine, and so on). I could have given a direct unreadable proof, but instead I decided to do it the right way, i.e., by introducing the restriction of scalars: given an algebra
SoverR, then anS-module is also anR-module, andS-linear maps induceR-linear maps and so on (which is the right way to say that a complex-differentiable function is also real-differentiable).Along the way, I needed to define some continuous linear functions on
ℂ(such as the real part or the imaginary part). I put them into a new fileanalysis/complex/basic, and refactored things a little bit by moving there facts about the complex numbers that were scattered around.