inner_product_apply_eigenvector — Mathlib

English

If T v = μ v, then the inner product ⟪v, T v⟫ equals μ times the squared norm of v.

Русский

Если T v = μ v, то ⟪v, T v⟫ равно μ умножить на норму v в квадрате.

LaTeX

$$$$ \langle v, T v \rangle = \mu \|v\|^2. $$$$

Lean4

theorem inner_product_apply_eigenvector {μ : 𝕜} {v : E} {T : E →ₗ[𝕜] E} (h : T v = μ • v) :
    ⟪v, T v⟫ = μ * (‖v‖ : 𝕜) ^ 2 := by simp only [h, inner_smul_right, inner_self_eq_norm_sq_to_K]

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