Cauchy_Bunyakovsky_Schwarz_Inequality
Provedalgebraanalysiscauchy-bunyakovsky-schwarz-inequalityinequalitiesintegral-calculuslinear-algebraproofwiki
The Cauchy-Bunyakovsky-Schwarz inequality for inner product spaces.
Preamble
import Mathlib.Analysis.InnerProductSpace.Basic import Mathlib.Tactic
Formal statement
theorem Cauchy_Bunyakovsky_Schwarz_Inequality {F : Type*} [RCLike F] {E : Type*} [SeminormedAddCommGroup E] [InnerProductSpace F E] (u v : E) : ‖@inner F E _ u v‖ ≤ ‖u‖ * ‖v‖ := by sorrySource