Theorems · Theorem · functional analysis

CStarAlgebra.nnnorm_sub_mul_self_le

∀ {A : Type u_2} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {x y : A} (z : A),
  0 ≤ x → y ∈ Set.Icc x 1 → ∀ {c : NNReal}, ‖star z * (1 - x) * z‖₊ ≤ c ^ 2 → ‖z - y * z‖₊ ≤ c

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.

Defined in

Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Cited by

1 results in Mathlib

Foundations

Depth 322 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CStarAlgebraPartialOrderStarOrderedRing