English
Let A be a C*-algebra with a compatible order and star, and let x,y ∈ A with 0 ≤ x ≤ y ≤ 1. Then for z ∈ A and c ∈ ℝ≥0, if ||star z · (1 − x) · z||₊ ≤ c², then ||z − y · z||₊ ≤ c.
Русский
Пусть A — C*-алгебра с совместимым порядком и сопряжением. Пусть x ≥ 0, x ≤ y ≤ 1 и z ∈ A, c ≥ 0. Если ||z* (1 − x) z||₊ ≤ c², то ||z − y z||₊ ≤ c.
LaTeX
$$$\forall z \in A, \; 0 \le x \le y \le 1, \; c \ge 0, \; \big\|\star z (1 - x) z\big\|_{+} \le c^{2} \Rightarrow \big\| z - y z \big\|_{+} \le c$$$
Lean4
/-- This is a common reasoning sequence in C⋆-algebra theory. If `0 ≤ x ≤ y ≤ 1`, then the norm of
`z - y * z` is controlled by the norm of `star z * (1 - x) * z`, which is advantageous because the
latter is nonnegative. This is a key step in establishing the existence of an increasing approximate
unit in general C⋆-algebras. -/
theorem nnnorm_sub_mul_self_le {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {x y : A} (z : A)
(hx₀ : 0 ≤ x) (hy : y ∈ Set.Icc x 1) {c : ℝ≥0} (h : ‖star z * (1 - x) * z‖₊ ≤ c ^ 2) : ‖z - y * z‖₊ ≤ c :=
by
nth_rw 1 [← one_mul z]
rw [← sqrt_sq c, le_sqrt_iff_sq_le, ← sub_mul, sq, ← CStarRing.nnnorm_star_mul_self]
simp only [star_mul, star_sub, star_one]
have hy₀ : y ∈ Set.Icc 0 1 := ⟨hx₀.trans hy.1, hy.2⟩
have hy' : 1 - y ∈ Set.Icc 0 1 := Set.sub_mem_Icc_zero_iff_right.mpr hy₀
rw [hy₀.1.star_eq, ← mul_assoc, mul_assoc (star _), ← sq]
refine nnnorm_le_nnnorm_of_nonneg_of_le (conjugate_nonneg (pow_nonneg hy'.1 2) _) ?_ |>.trans h
refine conjugate_le_conjugate ?_ _
trans (1 - y)
· simpa using pow_antitone hy'.1 hy'.2 one_le_two
· gcongr
exact hy.1
