English
Every element a ∈ A can be written as a linear combination with I^k coefficients of four nonnegative elements; i.e., a = x1 + i x2 − x3 − i x4 with xi ≥ 0 and ∥xi∥ ≤ ∥a∥.
Русский
Каждый элемент a ∈ A можно разложить как сумма четырех неотрицательных элементов с коэффициентами 1, i, −1, −i: a = x1 + i x2 − x3 − i x4, где xi ≥ 0 и ∥xi∥ ≤ ∥a∥.
LaTeX
$$$$\exists x_1, x_2, x_3, x_4 \in A,\ x_i \ge 0,\ \|x_i\| \le \|a\|\ (i=1,2,3,4) \ \text{ и } a = x_1 + i x_2 - x_3 - i x_4.$$$$
Lean4
theorem exists_sum_four_nonneg {A : Type*} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : A) :
∃ x : Fin 4 → A, (∀ i, 0 ≤ x i) ∧ (∀ i, ‖x i‖ ≤ ‖a‖) ∧ a = ∑ i : Fin 4, I ^ (i : ℕ) • x i :=
by
use ![(realPart a)⁺, (imaginaryPart a)⁺, (realPart a)⁻, (imaginaryPart a)⁻]
rw [← and_assoc, ← forall_and]
constructor
· intro i
fin_cases i
all_goals
constructor
· simp
cfc_tac
· exact CStarAlgebra.norm_posPart_le _ |>.trans <| realPart.norm_le a
· exact CStarAlgebra.norm_posPart_le _ |>.trans <| imaginaryPart.norm_le a
· exact CStarAlgebra.norm_negPart_le _ |>.trans <| realPart.norm_le a
· exact CStarAlgebra.norm_negPart_le _ |>.trans <| imaginaryPart.norm_le a
· nth_rw 1 [← CStarAlgebra.linear_combination_nonneg a]
simp only [Fin.sum_univ_four, Fin.coe_ofNat_eq_mod, Matrix.cons_val, Nat.reduceMod, I_sq, I_pow_three]
module
