PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.SharpEffect

Projections are sharp

i. Overview

A projection `p` is a sharp effect: it is not a proper mixture of two different effects. If `p = t y₁ + s y₂`, conjugating by `1 - p` kills both `y₁` and `y₂`, so by the C⋆-identity both commute with `p` and lie below it, which forces `y₁ = y₂ = p`.

ii. Key results

`IsIdempotentElem.isSharp` : idempotent effects are sharp.

2 declarations

theorem

$x, y \ge 0 \land x + y = 0 \implies x = 0$ in ordered additive groups

#nonneg_add_eq_zero

Let $A$ be a partially ordered additive group. For any two elements $x, y \in A$ such that $x$ and $y$ are nonnegative (i.e., $0 \le x$ and $0 \le y$ ), if their sum is zero ( $x + y = 0$ ), then $x = 0$ .

theorem

$b x b = 0 \implies \sqrt{x} b = 0$ for self-adjoint $b$ and $x \ge 0$

#sandwich_eq_zero

Let $b$ be a self-adjoint element and $x$ be a non-negative element ( $x \ge 0$ ) in a $C^*$ -algebra. If $b x b = 0$ , then $\sqrt{x} b = 0$ , where $\sqrt{x}$ denotes the square root of $x$ provided by the continuous functional calculus.