English
The real inner product on a real inner product space, viewed as a bilinear map E × E → ℝ, is bounded with bound 1; i.e., |⟪x,y⟫| ≤ ∥x∥ ∥y∥.
Русский
Данное скалярное произведение является ограниченной билинейной формой с границей 1: |⟪x,y⟫| ≤ ∥x∥ ∥y∥.
LaTeX
$$$\\text{IsBoundedBilinearMap}_{\\mathbb{R}} (x,y) = ⟪x,y⟫,\\quad |⟪x,y⟫| ≤ \\|x\\| \\|y\\|$$$
Lean4
/-- When an inner product space `E` over `𝕜` is considered as a real normed space, its inner
product satisfies `IsBoundedBilinearMap`.
In order to state these results, we need a `NormedSpace ℝ E` instance. We will later establish
such an instance by restriction-of-scalars, `InnerProductSpace.rclikeToReal 𝕜 E`, but this
instance may be not definitionally equal to some other “natural” instance. So, we assume
`[NormedSpace ℝ E]`.
-/
theorem _root_.isBoundedBilinearMap_inner [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] :
IsBoundedBilinearMap ℝ fun p : E × E => ⟪p.1, p.2⟫ :=
{ add_left := inner_add_left
smul_left := fun r x y => by simp only [← algebraMap_smul 𝕜 r x, algebraMap_eq_ofReal, inner_smul_real_left]
add_right := inner_add_right
smul_right := fun r x y => by simp only [← algebraMap_smul 𝕜 r y, algebraMap_eq_ofReal, inner_smul_real_right]
bound :=
⟨1, zero_lt_one, fun x y => by
rw [one_mul]
exact norm_inner_le_norm x y⟩ }
