English
For every x, the norm of innerSL applied to x equals the norm of x: ‖innerSL 𝕜 x‖ = ‖x‖.
Русский
Для любого x выполняется равенство норм: ‖innerSL 𝕜 x‖ = ‖x‖.
LaTeX
$$$\|innerSL\, 𝕜\, x\| = \|x\|$$$
Lean4
/-- `innerSL` is an isometry. Note that the associated `LinearIsometry` is defined in
`InnerProductSpace.Dual` as `toDualMap`. -/
@[simp]
theorem innerSL_apply_norm (x : E) : ‖innerSL 𝕜 x‖ = ‖x‖ :=
by
refine le_antisymm ((innerSL 𝕜 x).opNorm_le_bound (norm_nonneg _) fun y => norm_inner_le_norm _ _) ?_
rcases (norm_nonneg x).eq_or_lt' with (h | h)
· simp [h]
· refine (mul_le_mul_iff_left₀ h).mp ?_
calc
‖x‖ * ‖x‖ = ‖(⟪x, x⟫ : 𝕜)‖ := by rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]
_ ≤ ‖innerSL 𝕜 x‖ * ‖x‖ := (innerSL 𝕜 x).le_opNorm _
