coe_reApplyInnerSelf_apply — Mathlib

English

For symmetric T, the quantity ⟪T x, x⟫ is real for all x.

Русский

Для симметричного T величина ⟪T x, x⟫ вещественна для всех x.

LaTeX

$$$ \text{The value } ⟪T x, x⟫ \text{ is real for all } x$$$

Lean4

/-- For a symmetric operator `T`, the function `fun x ↦ ⟪T x, x⟫` is real-valued. -/
@[simp]
theorem coe_reApplyInnerSelf_apply {T : E →L[𝕜] E} (hT : IsSymmetric (T : E →ₗ[𝕜] E)) (x : E) :
    (T.reApplyInnerSelf x : 𝕜) = ⟪T x, x⟫ :=
  by
  rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ⟪T x, x⟫ = r
  · simp [hr, T.reApplyInnerSelf_apply]
  rw [← conj_eq_iff_real]
  exact hT.conj_inner_sym x x

Похожие утверждения