A preparation has zero entropy iff it is pure

Category: 3-Local (W4 of specs/qit-chain-scoping.md, the = 0 ↔ pure half).

W2 gave a preparation on Σ a von Neumann entropy (preparationEntropy, non-negative, at most log N); W3 made its density operator the barycentre of the rank-one projectors along the projective law. This module says when the entropy vanishes:

• vonNeumannEntropy_eq_zero_iff_outerProduct — the matrix-level characterisation (Mathlib/QuantumInfo/PureState.lean) in outerProduct form;
• trace_outerProduct_mul_barycenterMatrix — the overlap functional of a unit vector against a barycentre is the integral of the squared overlap;
• ★ ae_outerProduct_eq_of_barycenterMatrix_eq — a barycentre is a projector only if the law sits on one ray: if ∫ |rep p⟩⟨rep p| dμ = |φ⟩⟨φ| then almost every rep p lies on the ray of φ (the squared overlap integrates to one and is at most one, so it is one almost everywhere, the equality case of Cauchy–Schwarz);
• mk_eq_mk_of_outerProduct_eq, eq_dirac_of_ae_eq — two unit vectors with one projector span one ray; a probability measure concentrated on a point is the Dirac mass;
• ★★ preparationEntropy_eq_zero_iff — a preparation has zero entropy iff its projective law is a Dirac mass at a single ray, with the canonical measurable unit section (Projectivization.unitSection) as representative.

Honest scope

"Pure" here means the projective law of the preparation is concentrated on one ray. That is the operational notion (the density operator is a rank-one projector); it says nothing about the ontic preparation measure μprep itself beyond what its projection sees, and it is stated with the canonical section so that "the representative of the ray" is a definite object. The coarse-graining half of W4 (entropy is monotone under coarse-graining of regions) needs W8 (concavity) and is not here.

References: specs/qit-chain-scoping.md (W4); LF2/PreparationQdensity.lean (W2); LF2/PreparationBarycenter.lean (W3); Mathlib/QuantumInfo/PureState.lean; Mathlib/LinearAlgebra/Projectivization/UnitSection.lean.

Preparations of zero entropy are pure

theorem CSD.LF2.vonNeumannEntropy_eq_zero_iff_outerProduct {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ρ : Matrix ι ι ℂ} (hρ : ρ.PosSemidef) (htr : ρ.trace = 1) : QuantumInfo.vonNeumannEntropy ⋯ = 0 ↔ ∃ (ψ : EuclideanSpace ℂ ι), ‖ψ‖ = 1 ∧ ρ = outerProduct ψ

The outerProduct form of vonNeumannEntropy_eq_zero_iff.

theorem CSD.LF2.trace_outerProduct_mul_barycenterMatrix {Q : Type u_2} [MeasurableSpace Q] {N : ℕ} (rep : Q → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : Q), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (μ : MeasureTheory.Measure Q) [MeasureTheory.IsFiniteMeasure μ] (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) : (barycenterMatrix rep μ * outerProduct φ).trace = ↑(∫ (p : Q), ‖inner ℂ (rep p) φ‖ ^ 2 ∂μ)

The overlap functional of a fixed unit vector against a barycentre is the integral of the squared overlap.

theorem CSD.LF2.ae_outerProduct_eq_of_barycenterMatrix_eq {Q : Type u_2} [MeasurableSpace Q] {N : ℕ} (rep : Q → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : Q), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (μ : MeasureTheory.Measure Q) [MeasureTheory.IsProbabilityMeasure μ] (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) (h : barycenterMatrix rep μ = outerProduct φ) : ∀ᵐ (p : Q) ∂μ, outerProduct (rep p) = outerProduct φ

A barycentre is a projector only if the projective law sits on one ray. If the barycentre of |rep p⟩⟨rep p| along a probability measure is |φ⟩⟨φ|, then μ-almost every rep p lies on the ray of φ: the squared overlap integrates to one and is at most one (Cauchy–Schwarz), so it is one almost everywhere, which is the equality case.

theorem CSD.LF2.mk_eq_mk_of_outerProduct_eq {N : ℕ} {ψ φ : EuclideanSpace ℂ (Fin N)} (hψ : ‖ψ‖ = 1) (hφ : ‖φ‖ = 1) (h : outerProduct ψ = outerProduct φ) : Projectivization.mk ℂ ψ ⋯ = Projectivization.mk ℂ φ ⋯

Two unit vectors with the same projector span the same ray.

theorem CSD.LF2.eq_dirac_of_ae_eq {P : Type u_3} [MeasurableSpace P] (μ : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μ] {q : P} (h : ∀ᵐ (p : P) ∂μ, p = q) : μ = MeasureTheory.Measure.dirac q

A probability measure concentrated on a point is the Dirac mass.

The preparation-level statement

theorem CSD.LF2.preparationEntropy_eq_zero_iff {N : ℕ} {SigmaSpace : Type u_3} {G : Type u_4} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [Group G] [MulAction G SigmaSpace] [MulAction G (Projectivization ℂ (EuclideanSpace ℂ (Fin N)))] [MulAction.IsPretransitive G (Projectivization ℂ (EuclideanSpace ℂ (Fin N)))] (D : SectorData SigmaSpace (Projectivization ℂ (EuclideanSpace ℂ (Fin N))) G) (μFS : MeasureTheory.Measure (Projectivization ℂ (EuclideanSpace ℂ (Fin N)))) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] : preparationEntropy D μFS bridge μprep Projectivization.unitSection ⋯ ⋯ = 0 ↔ ∃ (q : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), MeasureTheory.Measure.map D.π μprep = MeasureTheory.Measure.dirac q

★★ A preparation has zero entropy iff it is pure. For a preparation on the projective sector, with the canonical measurable unit section as representative, the von Neumann entropy of its density operator vanishes iff its projective law is a Dirac mass at a single ray: zero entropy forces the barycentre to be a rank-one projector, which forces almost every ray of the preparation to be that projector's ray, which forces the law to be the Dirac mass there; conversely the barycentre along a Dirac mass is the projector of its ray.