𝕜 : Type u_1
E : Type u_2
F : Type ?u.519553
G : Type ?u.519556
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 (↑(↑adjoint A * A) x) x = inner (↑A x) (↑A x)
⊢ ‖↑A x‖ ^ 2 = ↑re (inner (↑(↑adjoint A * A) x) x)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.519553
G : Type ?u.519556
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 (↑(↑adjoint A * A) x) x)
have h : ⟪(A† * A) x, x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_left]; rfl
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.519553
G : Type ?u.519556
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 (↑(↑adjoint A * A) x) x = inner (↑A x) (↑A x)
⊢ ‖↑A x‖ ^ 2 = ↑re (inner (↑(↑adjoint A * A) x) x)
rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.519553
G : Type ?u.519556
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 (↑(↑adjoint A * A) x) x = inner (↑(↑adjoint A) (↑A x)) x
𝕜 : Type u_1
E : Type u_2
F : Type ?u.519553
G : Type ?u.519556
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 (↑(↑adjoint A * A) x) x = inner (↑A x) (↑A x)
rw [← adjoint_inner_left]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.519553
G : Type ?u.519556
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 (↑(↑adjoint A * A) x) x = inner (↑(↑adjoint A) (↑A x)) x
rfl