apply_norm_sq_eq_inner_adjoint_left

English

A formal proof shows that the adjointAux inner_left identity holds, using delta definitions and symmetry properties of dual maps.

Русский

Формальное доказательство демонстрирует истинность тождества для adjointAux inner_left через определения δ и симметрии двойственных отображений.

LaTeX

$$$$ \\langle \\mathrm{adjointAux} A \\; y, x \\rangle = \\langle y, A x \\rangle. $$$$

Lean4

theorem apply_norm_sq_eq_inner_adjoint_left (A : E →L[𝕜] F) (x : E) : ‖A x‖ ^ 2 = re ⟪(A† ∘L A) x, x⟫ :=
  by
  have h : ⟪(A† ∘L A) x, x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_left]; rfl
  rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]

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