Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 15 research declarations. Search 10,000 more complete Mathlib declarations.
15 results
Clear filtersoperator_ineq_SSA
Plain-language statement
Operator extension of SSA (Main result of Lin-Kim-Hsieh). For positive definite ρ_AB and σ_BC: ρ_A⁻¹ ⊗ σ_BC ≤ ρ_AB⁻¹ ⊗ σ_C where ρ_A = Tr_B(ρ_AB) and σ_C = Tr_B(σ_BC), and the RHS is reindexed via the associator (dA × dB) × dC ≃ dA × (dB × dC).
Source project: quantumInfo
Person-level attribution pending.
PosDef_traceRight
Plain-language statement
The partial trace (left) of a positive definite matrix is positive definite.
Source project: quantumInfo
Person-level attribution pending.
Sᵥₙ_pure_tripartite_triangle
Plain-language statement
Triangle inequality for pure tripartite states: S(A) ≤ S(B) + S(C).
Source project: quantumInfo
Person-level attribution pending.
Sᵥₙ_strong_subadditivity
Plain-language statement
Strong subadditivity on a tripartite system
Source project: quantumInfo
Person-level attribution pending.
Sᵥₙ_subadditivity
Plain-language statement
"Ordinary" subadditivity of von Neumann entropy
Source project: quantumInfo
Person-level attribution pending.
Sᵥₙ_wm
Plain-language statement
Weak monotonicity, version with partial traces.
Source project: quantumInfo
Person-level attribution pending.