-
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_space/of_norm): Create an inner product from a norm #4798
Conversation
@hrmacbeth For |
80e7031
to
5ebc57a
Compare
@hrmacbeth I finished |
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.
The title of the PR has nothing to do with its content, right?
# Inner product space derived from a norm | ||
|
||
This file defines an `inner_product_space` instance from a norm that respects the | ||
parallellogram identity. |
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.
Could you recall here what the parallelogram identity is? And maybe sketch the proof you will be giving somewhere in the file-level docstring, with pointers to intermediate lemmas in the proof.
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've recalled what the parallelogram identity is, but I can't link to intermediate lemmas because we're making them private.
@@ -0,0 +1,407 @@ | |||
/- | |||
Copyright (c) 2020 Heather Macbeth. All rights reserved. |
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.
2020??!!
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.
Zombie PR, revived by Ruben :)
4⁻¹ * ((𝓚 ‖x + y‖) * (𝓚 ‖x + y‖) - (𝓚 ‖x - y‖) * (𝓚 ‖x - y‖) | ||
+ (I:𝕜) * (𝓚 ‖(I:𝕜) • x + y‖) * (𝓚 ‖(I:𝕜) • x + y‖) | ||
- (I:𝕜) * (𝓚 ‖(I:𝕜) • x - y‖) * (𝓚 ‖(I:𝕜) • x - y‖)) |
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.
Does this generalize as an approach to producing a conjugate-linear map over any star ring? My guess would be that summing over the generators does the trick...
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 don't know much about star rings. Can you detail? How are the generators denoted in mathlib?
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 guess what I probably meant here is "over the quaternions".
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.
Probably you're right, but I have no idea how to do it in Lean. You will need to give me more info.
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 should be clear that this comment is not intended to block this PR
Apart from the merge-conflict this should be good, right? @Ruben-VandeVelde |
Certainly as far as I'm concerned |
LGTM modulo adding a sketch of the proof to the module docstring. Thank you! |
✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with |
Yury, did you mean to delegate to Heather? She's been inactive on that PR for 2 years and a half. |
Wow, a PR with an id that's less than the current Mathlib4 PRs :-) bors r+ |
…rom a norm (#4798) A normed space respecting the polarization identity is an inner product space. Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
A normed space respecting the polarization identity is an inner product space.
Co-authored-by: Frédéric Dupuis dupuisf@iro.umontreal.ca
Co-authored-by: Ruben Van de Velde 65514131+Ruben-VandeVelde@users.noreply.github.com
The idea will be to show that with this definition the dual space is indeed an inner product space. But many purely algebraic calculations remain, so this is WIP until I, Frédéric or any other volunteer has time to try them.
Separated out from #4379 (but independent of it). Discussion at
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Hilbert.20space.20is.20isometric.20to.20its.20dual