EffectGleason · section of the QIQT-H book

QIQTH.EffectGleason

← all sections · ← DifferentialAreaLaw · EinsteinEquationOfState →

EffectGleason · entries 74–76 of 1000

Definition 74 (IsEffect).  source ↗

An effect is a positive-semidefinite matrix E with 1 - E also PSD, i.e. 0 ≤ E ≤ 1 in the Löwner order — the yes-part of a POVM.

IsEffect d E  :=  E.PosSemidef∧(1−E).PosSemidef\mathrm{IsEffect}\,d\,E \;:=\; E.\mathrm{PosSemidef} \wedge (1 - E).\mathrm{PosSemidef}

Used by finite_noCollapseBorn_fromNoncontextuality.

Lemma 75 (EffectMeasure).  source ↗

A finite effect measure (generalized probability measure on effects): normalized, nonnegative, and effect-algebra (partially) additive — additive on coexistent pairs E, F (those with E + F still an effect, i.e. E + F ≤ 1). This is the standard Busch/CFMR hypothesis; effect-Gleason gives μ E = tr(ρ E).

N→Type\mathbb{N} \to Type

Proof. Immediate from the definitions. □\square

Used by finite_noCollapseBorn_fromNoncontextuality, μ.

Definition 76 (μ).  source ↗

μ d self  :=  self.1\mu\,d\,\mathrm{self} \;:=\; \mathrm{self}.1

Used by finite_noCollapseBorn_fromNoncontextuality.

← all sections · ← DifferentialAreaLaw · EinsteinEquationOfState →