English
A variant of the previous bound replacing the nonnegative norm by the usual norm: for all z,x,y as above and c ∈ ℝ with hc ≥ 0, if ||star z (1 − x) z|| ≤ c² then ||z − y z|| ≤ c.
Русский
Вариант предыдущего неравенства: заменяем неотрицательную норму на обычную норму. При тех же условиях и с c ∈ ℝ, если ||z* (1 − x) z|| ≤ c², то ||z − y z|| ≤ c.
LaTeX
$$$\forall z \in A, \; 0 \le x \le y \le 1, \; c \in \mathbb{R}, \; c \ge 0, \; \big\|\star z (1 - x) z\big\| \le c^{2} \Rightarrow \big\| z - y z \big\| \le c$$$
Lean4
/-- A variant of `nnnorm_sub_mul_self_le` which uses `‖·‖` instead of `‖·‖₊`. -/
theorem norm_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 : ℝ} (hc : 0 ≤ c) (h : ‖star z * (1 - x) * z‖ ≤ c ^ 2) : ‖z - y * z‖ ≤ c :=
nnnorm_sub_mul_self_le z hx₀ hy h (c := ⟨c, hc⟩)
