Commit 2021-01-05 16:18 a6633e5b
View on Github →feat(analysis/normed_space/inner_product): new versions of Cauchy-Schwarz equality case (#5586)
The existing version of the Cauchy-Schwarz equality case characterizes the pairs x, y with abs ⟪x, y⟫ = ∥x∥ * ∥y∥. This PR provides a characterization, with converse, of pairs satisfying ⟪x, y⟫ = ∥x∥ * ∥y∥, and some consequences.