English
In a unital C*-algebra, every element x is a finite complex linear combination of four unitary elements, with coefficients bounded in norm by ∥x∥/2.
Русский
В унитальной C*-алгебре любой элемент x является линейной комбинацией четырех унитарных элементов, коэффициенты имеют норму не более ∥x∥/2.
LaTeX
$$$\exists u: (\mathsf{Fin}\,4 \to \text{unitary }A), \exists c: (\mathsf{Fin}\,4 \to \mathbb{C}), x = \sum_{i=1}^4 c_i u_i, \; \forall i, \|c_i\| \le \|x\|/2$$$
Lean4
/-- Every element `x` in a unital C⋆-algebra is a linear combination of four unitary elements,
and the norm of each coefficient does not exceed `‖x‖ / 2`. -/
theorem exists_sum_four_unitary (x : A) :
∃ u : Fin 4 → unitary A, ∃ c : Fin 4 → ℂ, x = ∑ i, c i • (u i : A) ∧ ∀ i, ‖c i‖ ≤ ‖x‖ / 2 :=
by
let _ := CStarAlgebra.spectralOrder
let _ := CStarAlgebra.spectralOrderedRing
obtain (rfl | hx) := eq_or_ne x 0
· exact ⟨![1, -1, 1, -1], 0, by simp⟩
· have := norm_smul_two_inv_smul_add_four_unitary x hx
extract_lets u₁ u₂ at this
use ![u₁, star u₁, u₂, star u₂], ![‖x‖ * 2⁻¹, ‖x‖ * 2⁻¹, ‖x‖ * 2⁻¹ * I, ‖x‖ * 2⁻¹ * I]
constructor
· conv_lhs => rw [this]
simp [Fin.sum_univ_four, ← Complex.coe_smul]
module
· intro i
fin_cases i
all_goals simp [div_eq_mul_inv]
