Lemma 2: A Basic Unitary Identity

For any linear isometry U on a Hilbert space and any vector h: 2 Re⟨h, Uh⟩ = 2‖h‖² - ‖h - Uh‖²

Reference: lamportform.tex, Lemma 1.2 (lem:unitary), lines 166–191.

theorem ConnesLean.unitary_identity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (U : E →ₗᵢ[ℂ] E) (h : E) : 2 * RCLike.re (inner ℂ h (U h)) = 2 * ‖h‖ ^ 2 - ‖h - U h‖ ^ 2

Lemma 2 (Basic unitary identity): For any linear isometry U on a Hilbert space and any vector h, 2 Re⟨h, Uh⟩ = 2‖h‖² - ‖h - Uh‖².

Reference: lamportform.tex, Lemma 1.2, lines 166–191.

Note: We state this for a LinearIsometry, which captures the isometric property ‖Uh‖ = ‖h‖ used in Step 2 of the proof. Unitarity (surjectivity) is not needed for this identity.

theorem ConnesLean.unitary_identity' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (U : E ≃ₗᵢ[ℂ] E) (h : E) : 2 * RCLike.re (inner ℂ h (U h)) = 2 * ‖h‖ ^ 2 - ‖h - U h‖ ^ 2

Variant of the unitary identity using LinearIsometryEquiv (i.e., a truly unitary operator).

theorem ConnesLean.unitary_identity_id {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (h : E) : 2 * RCLike.re (inner ℂ h h) = 2 * ‖h‖ ^ 2

Corollary: When U = id, we get 2 Re⟨h, h⟩ = 2‖h‖².

Proof: re ⟪h, h⟫ = ‖h‖² by inner_self_eq_norm_sq.