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 9 research declarations. Search 10,000 more complete Mathlib declarations.
9 results
Clear filtersMState.purify_spec
Plain-language statement
The defining property of purification, that tracing out the purifying system gives the original mixed state.
Source project: quantumInfo
Person-level attribution pending.
MState.spectrum_prod
Plain-language statement
Spectrum of direct product. There is a permutation σ so that the spectrum of the direct product of ρ₁ and ρ₂, as permuted under σ, is the pairwise products of the spectra of ρ₁ and ρ₂.
Source project: quantumInfo
Person-level attribution pending.
MState.spectrum_pure_eq_constant
Plain-language statement
The specturm of a pure state is (1,0,0,...), i.e. a constant distribution.
Source project: quantumInfo
Person-level attribution pending.