theorem CommutingRepetition.norm_normalize_sub_normalize_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (v w : E) (hv : v ≠ 0) (hw : w ≠ 0) : ‖↑‖v‖⁻¹ • v - ↑‖w‖⁻¹ • w‖ ≤ 2 * ‖v - w‖ / ‖v‖

Difference of normalizations against difference of vectors (05_prerounding.tex, eq prerounding-normalization-inequality, linear form): ‖v/‖v‖ − w/‖w‖‖ ≤ 2‖v−w‖/‖v‖.

theorem CommutingRepetition.norm_normalize_sub_normalize_sq_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (v w : E) (hv : v ≠ 0) (hw : w ≠ 0) : ‖↑‖v‖⁻¹ • v - ↑‖w‖⁻¹ • w‖ ^ 2 ≤ 4 * ‖v - w‖ ^ 2 / ‖v‖ ^ 2

Normalization inequality (05_prerounding.tex, eq prerounding-normalization-inequality): for nonzero vectors, ‖v/‖v‖ − w/‖w‖‖² ≤ 4·‖v−w‖²/‖v‖².

theorem CommutingRepetition.abs_re_inner_effect_sub_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : H →L[ℂ] H) (h0 : 0 ≤ T) (h1 : T ≤ 1) (v w : H) (hv : ‖v‖ = 1) (hw : ‖w‖ = 1) : |(inner ℂ v (T v)).re - (inner ℂ w (T w)).re| ≤ 2 * ‖v - w‖

Effect-evaluation Lipschitz bound (02_preliminaries.tex: "If v, w are unit vectors and 0 ≤ T ≤ 1, then |⟨v,Tv⟩ − ⟨w,Tw⟩| ≤ 2‖v−w‖"). Stated for the Loewner order on bounded operators; consumed by the section-6 assembly.

Cauchy–Schwarz for positive semidefinite forms and the

POVM-output ℓ¹ estimate (06_otqcs.tex, eq vector-to-l1)

theorem CommutingRepetition.abs_inner_positive_form_sq_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →L[ℂ] H) (hsa : ∀ (x y : H), inner ℂ (T x) y = inner ℂ x (T y)) (hpos : ∀ (x : H), 0 ≤ (inner ℂ x (T x)).re) (x y : H) : ‖inner ℂ x (T y)‖ ^ 2 ≤ (inner ℂ x (T x)).re * (inner ℂ y (T y)).re

Cauchy–Schwarz for the semidefinite form of a positive self-adjoint operator: ‖⟪x, T y⟫‖² ≤ re ⟪x, T x⟫ · re ⟪y, T y⟫. Proved through PreInnerProductSpace.Core (no definiteness needed).

theorem CommutingRepetition.abs_inner_positive_form_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →L[ℂ] H) (hsa : ∀ (x y : H), inner ℂ (T x) y = inner ℂ x (T y)) (hpos : ∀ (x : H), 0 ≤ (inner ℂ x (T x)).re) (x y : H) : ‖inner ℂ x (T y)‖ ≤ √(inner ℂ x (T x)).re * √(inner ℂ y (T y)).re

Square-root form of the positive-form Cauchy–Schwarz.

theorem CommutingRepetition.sum_abs_re_inner_effect_sub_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] (T : ι → H →L[ℂ] H) (hsa : ∀ (i : ι) (x y : H), inner ℂ ((T i) x) y = inner ℂ x ((T i) y)) (hpos : ∀ (i : ι) (x : H), 0 ≤ (inner ℂ x ((T i) x)).re) (hsum : ∑ i : ι, T i = 1) (z u : H) (hz : ‖z‖ = 1) (hu : ‖u‖ = 1) : ∑ i : ι, |(inner ℂ z ((T i) z)).re - (inner ℂ u ((T i) u)).re| ≤ 2 * ‖z - u‖

POVM-output ℓ¹ estimate (06_otqcs.tex, eq vector-to-l1, consumed form): for a finite family of positive self-adjoint operators summing to the identity and two unit vectors, the ℓ¹ distance of the two output laws is at most 2 ‖z − u‖.