𝕜 : Type u_1
E : Type u_2
F : Type ?u.658805
G : Type ?u.658808
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
h : inner x (↑(↑adjoint A * A) x) = inner (↑A x) (↑A x)
⊢ ‖↑A x‖ ^ 2 = ↑re (inner x (↑(↑adjoint A * A) x))
𝕜 : Type u_1
E : Type u_2
F : Type ?u.658805
G : Type ?u.658808
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ ‖↑A x‖ ^ 2 = ↑re (inner x (↑(↑adjoint A * A) x))
have h : ⟪x, (A† * A) x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_right]; rfl
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.658805
G : Type ?u.658808
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
h : inner x (↑(↑adjoint A * A) x) = inner (↑A x) (↑A x)
⊢ ‖↑A x‖ ^ 2 = ↑re (inner x (↑(↑adjoint A * A) x))
rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.658805
G : Type ?u.658808
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ inner x (↑(↑adjoint A * A) x) = inner x (↑(↑adjoint A) (↑A x))
𝕜 : Type u_1
E : Type u_2
F : Type ?u.658805
G : Type ?u.658808
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ inner x (↑(↑adjoint A * A) x) = inner (↑A x) (↑A x)
rw [← adjoint_inner_right]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.658805
G : Type ?u.658808
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ inner x (↑(↑adjoint A * A) x) = inner x (↑(↑adjoint A) (↑A x))
rfl