English
For x ≠ 0 in a C*-algebra, there exist four unitaries u1, u2, u3, u4 such that x equals a real scalar multiple of (u1 + u1* + i(u2 + u2*)). Moreover, the norm of the coefficients is controlled by ∥x∥/2.
Русский
Пусть x ≠ 0 в C*-алгебре; найдутся четыре унитарных элемента u1,u2,u3,u4 такие, что x = ∥x∥·(2⁻¹)(u1 + u1* + i(u2 + u2*)) и |coefficients| ≤ ∥x∥/2.
LaTeX
$$$\exists u_1,u_2,u_3,u_4\colon\text{unitary }A,\ \exists \alpha_i \in \mathbb{C}: x = \|x\|\,2^{-1}(u_1 + u_1^* + i(u_2 + u_2^*))$, with each $|\alpha_i| \le \|x\|/2$$$
Lean4
/-- A stepping stone to `CStarAlgebra.exists_sum_four_unitary` that specifies the unitary
elements precisely. The `let`s in the statement are intentional. -/
theorem norm_smul_two_inv_smul_add_four_unitary (x : A) (hx : x ≠ 0) :
let u₁ : unitary A :=
selfAdjoint.unitarySelfAddISMul (ℜ (‖x‖⁻¹ • x))
(by simpa [norm_smul, inv_mul_le_one₀ (norm_pos_iff.2 hx)] using realPart.norm_le x)
let u₂ : unitary A :=
selfAdjoint.unitarySelfAddISMul (ℑ (‖x‖⁻¹ • x))
(by simpa [norm_smul, inv_mul_le_one₀ (norm_pos_iff.2 hx)] using imaginaryPart.norm_le x)
x = ‖x‖ • (2⁻¹ : ℝ) • (u₁ + star u₁ + I • (u₂ + star u₂) : A) :=
by
intro u₁ u₂
rw [smul_add, smul_comm _ I, unitary.coe_star, unitary.coe_star, ← realPart_apply_coe (u₁ : A), ←
realPart_apply_coe (u₂ : A)]
simpa only [u₁, u₂, selfAdjoint.realPart_unitarySelfAddISMul, realPart_add_I_smul_imaginaryPart] using
Eq.symm <| NormedSpace.norm_smul_normalize x
