English
For an element a in a C*-algebra, the following are equivalent: a ≥ 0; a = sqrt(a) sqrt(a); ∃ b ≥ 0 with a = b^2; ∃ b self-adjoint with a = b^2; ∃ b with a = b^* b; ∃ b with a = b b^*; a is self-adjoint and has nonnegative spectrum.
Русский
Для элемента a в алгебре C*- выполняются эквивалентности: a ≥ 0; a = sqrt(a) sqrt(a); ∃ b ≥ 0 с a = b^2; ∃ b самособранный с a = b^2; ∃ b с a = b^* b; ∃ b с a = b b^*; a самособран и имеет неотрицательный спектр.
LaTeX
$$$0 \\le a \\iff a = \\sqrt a \\sqrt a \\iff \\exists b\\ (0 \\le b \\wedge a = b^2) \\\\ \\\\ \\iff \\exists b\\ (IsSelfAdjoint b \\wedge a = b^2) \\\\ \\\\ \\iff \\exists b\\ (a = b^* b) \\\\ \\\\ \\iff \\exists b\\ (a = b b^*) \\\\ \\\\ \\iff IsSelfAdjoint(a) \\wedge \\text{QuasispectrumRestricts}(a,\\mathbb{R}).$$$
Lean4
/-- For an element `a` in a C⋆-algebra, TFAE:
* `0 ≤ a`
* `a = sqrt a * sqrt a`
* `a = b * b` for some nonnegative `b`
* `a = b * b` for some self-adjoint `b`
* `a = star b * b` for some `b`
* `a = b * star b` for some `b`
* `a` is self-adjoint and has nonnegative spectrum -/
theorem _root_.CStarAlgebra.nonneg_TFAE {a : A} :
[0 ≤ a, a = sqrt a * sqrt a, ∃ b : A, 0 ≤ b ∧ a = b * b, ∃ b : A, IsSelfAdjoint b ∧ a = b * b,
∃ b : A, a = star b * b, ∃ b : A, a = b * star b,
IsSelfAdjoint a ∧ QuasispectrumRestricts a ContinuousMap.realToNNReal].TFAE :=
by
tfae_have 1 ↔ 7 := nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts
tfae_have 1 → 2 := fun h => sqrt_mul_sqrt_self a |>.symm
tfae_have 2 → 3 := fun h => ⟨sqrt a, sqrt_nonneg a, h⟩
tfae_have 3 → 4 := fun ⟨b, hb⟩ => ⟨b, hb.1.isSelfAdjoint, hb.2⟩
tfae_have 4 → 5 := fun ⟨b, hb⟩ => ⟨b, hb.1.symm ▸ hb.2⟩
tfae_have 5 → 6 := fun ⟨b, hb⟩ => ⟨star b, star_star b |>.symm ▸ hb⟩
tfae_have 6 → 1 := fun ⟨b, hb⟩ => hb ▸ mul_star_self_nonneg _
tfae_finish
