-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(analysis/inner_product/calculus): [higher] differentiability to/from euclidean_space
#15363
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In principle, this could also be done for pi_Lp
. No need to do that in this PR, but could you mention it as a TODO? Also please mention your lemmas in the module docstring of analysis/inner_product_space/calculus
.
{n : with_top ℕ} : | ||
cont_diff_on 𝕜 n f t ↔ ∀ i, cont_diff_on 𝕜 n (λ x, f x i) t := | ||
begin | ||
let φ : euclidean_space 𝕜 ι ≃L[𝕜] ι → 𝕜 := (linear_equiv.refl _ _).to_continuous_linear_equiv, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This ought to be called pi_Lp.continuous_linear_equiv
or pi_Lp.equivL
or something; expecially since you used it in all of these lemmas!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I added the euclidean_space
version because rw
was giving me a hard time using a general pi_Lp
version
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have some cosmetic comments, but otherwise LGTM!
bors d+
✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
Canceled. |
bors merge |
…from `euclidean_space` (#15363) This duplicates some of the calculus `pi` API to `euclidean_space`. Namely : - we duplicate all the variants of `differentiable_pi` to show that a function to a euclidean space is (higher) differentiable iff all of its components are - we introduce `euclidean_version.proj`, analogous to `continuous_linear_map.proj`. This allows us to avoid duplicating all the `differentiable_apply`-like lemmas, because one can just use the API for smoothness of continuous linear maps Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Pull request successfully merged into master. Build succeeded: |
euclidean_space
euclidean_space
…from `euclidean_space` (#15363) This duplicates some of the calculus `pi` API to `euclidean_space`. Namely : - we duplicate all the variants of `differentiable_pi` to show that a function to a euclidean space is (higher) differentiable iff all of its components are - we introduce `euclidean_version.proj`, analogous to `continuous_linear_map.proj`. This allows us to avoid duplicating all the `differentiable_apply`-like lemmas, because one can just use the API for smoothness of continuous linear maps Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
This duplicates some of the calculus
pi
API toeuclidean_space
. Namely :differentiable_pi
to show that a function to a euclidean space is (higher) differentiable iff all of its components areeuclidean_version.proj
, analogous tocontinuous_linear_map.proj
. This allows us to avoid duplicating all thedifferentiable_apply
-like lemmas, because one can just use the API for smoothness of continuous linear maps