-
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/normed_space/inner_product): Cauchy-Schwarz equality case and other lemmas #4571
Conversation
Note that #4379 depends on this PR. |
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 left some comments, especially aiming at gettind rid of @... _ _ _ _
which I always find not good looking.
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Thanks! I've also thrown in the warning about |
bors merge |
@@ -118,6 +118,9 @@ scalar product. This is what we implement in this paragraph, starting from a str | |||
Our goal here is not to develop a whole theory with all the supporting API, as this will be done | |||
below for `inner_product_space`. Instead, we implement the bare minimum to go as directly as | |||
possible to the construction of the norm and the proof of the triangular inequality. | |||
|
|||
Warning: Do not use this `core` structure if the space you are interested in already has a norm | |||
instance defined on it, otherwise this will create a second non-defeq norm instance! |
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 think the suggestion was for the warning to go on the of_core
constructor itself. Of course, it's good to warn in as many places as possible.
…se and other lemmas (#4571) Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
This PR generalizes the Cauchy-Schwarz equality case to the complex case via
is_R_or_C
. It also adds a few other lemmas related to orthogonal subspaces, and fixes a few bugs.