LF2: Mixed-state Born rule and spectral ensemble on the indexed density type

Category: 2-Local (the operational density-operator layer).

The mixed-state ensemble content (SigmaLayer/MixedEnsemble.lean) was proved for DensityOperator N (indexed by Fin N). This module ports it to the composite index-parametric density type DensityOperatorIx ι (LF2/ReducedDensity.lean, indexed by an arbitrary [Fintype ι] [DecidableEq ι]) — the type the bipartite / composite interface (SigmaLayer/CompositeInterface.lean, target T9) uses via reduced / reducedLeft partial traces. This closes the reported density-matrix gap: mixed-state Born on the composite indexed type, not only on Fin N.

Main results

• DensityOperatorIx.traceForm : the Born pairing Tr(ρ E) on the indexed type.
• DensityOperatorIx.ensemble + traceForm_ensemble : finite convex ensembles of indexed densities are indexed densities, with an affine Born rule.
• DensityOperatorIx.eq_eigen_ensemble + eigenvalues_isProbability : every indexed density is ∑ᵢ λᵢ |eᵢ⟩⟨eᵢ| for a probability distribution λ (spectral theorem).
• DensityOperatorIx.mixedEnsemble_capstone : the mixed Born rule is the eigenvalue-weighted average of the pure Born rules — on the composite indexed type.

The proofs are the faithful ι-generalisation of the Fin N originals; every underlying lemma (Matrix.posSemidef_sum, the Hermitian spectral theorem, trace_eq_sum_eigenvalues, eigenvalues_nonneg) is stated for a general Fintype index.

noncomputable def CSD.LF2.DensityOperatorIx.traceForm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : DensityOperatorIx ι) (E : Matrix ι ι ℂ) : ℝ

Born pairing on the indexed density type. Tr(ρ E) as a real number.

Equations

• ρ.traceForm E = RCLike.re (ρ.M * E).trace

A — the affine convex ensemble

noncomputable def CSD.LF2.DensityOperatorIx.ensemble {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : Type u_2} [Fintype κ] (w : κ → ℝ) (hw : ∀ (k : κ), 0 ≤ w k) (hsum : ∑ k : κ, w k = 1) (ρ : κ → DensityOperatorIx ι) : DensityOperatorIx ι

Finite convex ensemble of indexed densities. For a probability distribution w and indexed densities ρ : κ → DensityOperatorIx ι, the convex combination ∑ₖ wₖ ρₖ is an indexed density.

Equations

• CSD.LF2.DensityOperatorIx.ensemble w hw hsum ρ = { M := ∑ k : κ, ↑(w k) • (ρ k).M, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }

@[simp]

theorem CSD.LF2.DensityOperatorIx.ensemble_M {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : Type u_2} [Fintype κ] (w : κ → ℝ) (hw : ∀ (k : κ), 0 ≤ w k) (hsum : ∑ k : κ, w k = 1) (ρ : κ → DensityOperatorIx ι) : (ensemble w hw hsum ρ).M = ∑ k : κ, ↑(w k) • (ρ k).M

theorem CSD.LF2.DensityOperatorIx.traceForm_ensemble {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : Type u_2} [Fintype κ] (w : κ → ℝ) (hw : ∀ (k : κ), 0 ≤ w k) (hsum : ∑ k : κ, w k = 1) (ρ : κ → DensityOperatorIx ι) (E : Matrix ι ι ℂ) : (ensemble w hw hsum ρ).traceForm E = ∑ k : κ, w k * (ρ k).traceForm E

The Born rule is affine over the ensemble (indexed type): mixing preparations mixes the outcome probabilities, Tr((∑ₖ wₖ ρₖ) E) = ∑ₖ wₖ Tr(ρₖ E).

B — the spectral ensemble decomposition (mixed = ensemble of pure)

noncomputable def CSD.LF2.DensityOperatorIx.outerProduct {ι : Type u_1} (φ : EuclideanSpace ℂ ι) : Matrix ι ι ℂ

Rank-one outer product |φ⟩⟨φ| on the index ι.

Equations

• CSD.LF2.DensityOperatorIx.outerProduct φ = Matrix.vecMulVec (fun (i : ι) => φ.ofLp i) fun (i : ι) => star (φ.ofLp i)

theorem CSD.LF2.DensityOperatorIx.eq_eigen_ensemble {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : DensityOperatorIx ι) : ρ.M = ∑ i : ι, ↑(⋯.eigenvalues i) • outerProduct (⋯.eigenvectorBasis i)

Every indexed density is the eigenvalue-weighted sum of its eigenvector projectors: ρ = ∑ᵢ λᵢ |eᵢ⟩⟨eᵢ|. From the Hermitian spectral theorem.

theorem CSD.LF2.DensityOperatorIx.eigenvalues_isProbability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : DensityOperatorIx ι) : (∀ (i : ι), 0 ≤ ⋯.eigenvalues i) ∧ ∑ i : ι, ⋯.eigenvalues i = 1

The eigenvalues of an indexed density form a probability distribution.

theorem CSD.LF2.DensityOperatorIx.mixedEnsemble_capstone {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : DensityOperatorIx ι) (E : Matrix ι ι ℂ) : ρ.traceForm E = ∑ i : ι, ⋯.eigenvalues i * RCLike.re (outerProduct (⋯.eigenvectorBasis i) * E).trace

The mixed Born rule is the eigenvalue-weighted average of the pure Born rules (composite indexed type): Tr(ρ E) = ∑ᵢ λᵢ Tr(|eᵢ⟩⟨eᵢ| E). Combines the spectral decomposition with the affine Born rule — closing T9 on DensityOperatorIx.