Research proof index

Monotonicity of the trace functional under partial trace for α > 1. Equation (2.8) of the paper (second line).

Twirling on a bipartite system: applying 1_A ⊗ V_i and averaging produces the -- partial trace tensored with the maximally mixed state. -/ -- theorem twirling_bipartite [Nonempty dB] -- (κ : Type) [Fintype κ] (V : κ → Matrix.unitaryGroup dB ℂ) -- (hV : ∀ (X : HermitianMat dB ℂ), -- (Fintype.card κ : ℝ)⁻¹ • ∑ i : κ, X.conj (V i : Matrix dB dB ℂ) = -- (X....

The support projection of A acts as identity on B when A.ker ≤ B.ker. Since A.supportProj projects onto ker(A)⊥ and B is zero on ker(A), the projection preserves B.

The SupRegularized value is also lower bounded.

For Monotone functions, the SupRegularized is the supremum of values.

Entanglement of Formation of bipartite systems. It is the convex roof extension of the von Neumann entropy of one of the subsystems (here chosen to be the left one, but see Entropy.Sᵥₙ_of_partial_eq). The function Sᵥₙ ∘ traceRight ∘ pure is phase-invariant because pure maps phase-equivalent kets to the same mixed state, so it descends to `KetUpToPha...