English
A C*-algebra is spanned by nonnegative elements of norm at most r: span_ℂ({x ∈ A | 0 ≤ x} ∩ closedBall(0, r)) = ⊤ for r > 0.
Русский
C*-алгебра порождается неотрицательными элементами нормой не более r: линейная оболочка этих элементов равна всей алгебре, если r > 0.
LaTeX
$$$$\operatorname{span}_{\mathbb{C}}\big\{ x \in A \\ 0 \le x \\ \|x\| \le r \big\} = \top, \quad r > 0.$$$$
Lean4
/-- A C⋆-algebra is spanned by nonnegative elements of norm at most `r` -/
theorem span_nonneg_inter_closedBall {r : ℝ} (hr : 0 < r) : span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r) = ⊤ :=
by
rw [eq_top_iff, ← span_nonneg, span_le]
intro x hx
obtain (rfl | hx_pos) := eq_zero_or_norm_pos x
· exact zero_mem _
· suffices (r * ‖x‖⁻¹ : ℂ)⁻¹ • ((r * ‖x‖⁻¹ : ℂ) • x) = x
by
rw [← this]
refine smul_mem _ _ (subset_span <| Set.mem_inter ?_ ?_)
· norm_cast
exact smul_nonneg (by positivity) hx
· simp [mul_smul, norm_smul, abs_of_pos hr, inv_mul_cancel₀ hx_pos.ne']
apply inv_smul_smul₀
norm_cast
positivity
