Commit 2026-02-17 19:29 85b30bca
View on Github →feat(Analysis/InnerProductSpace/Basic): variants of the parallelogram law with squaring (#35171)
This PR adds a couple variants of the parallelogram law written in terms of squaring ‖x + y‖ ^ 2 + ‖x - y‖ ^ 2 rather than multiplication ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖. I've found these to be helpful in practice.
I renamed the existing statements per @hrmacbeth's suggestion.