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 115 research declarations. Search 10,000 more complete Mathlib declarations.
115 results
Clear filtersMState.PosDef_mix_of_ne_one
Plain-language statement
If the second state is positive definite and the mixture is nondegenerate, their mixture is also positive definite.
Source project: quantumInfo
Person-level attribution pending.
MState.pure_iff_rank_eq_one
Plain-language statement
A mixed state is pure if and only if its rank is 1.
Source project: quantumInfo
Person-level attribution pending.
MState.pure_of_constant_spectrum
Plain-language statement
If the specturm of a mixed state is (1,0,0...) i.e. a constant distribution, it is a pure state.
Source project: quantumInfo
Person-level attribution pending.
MState.pure_separable_iff_traceLeft_pure
Plain-language statement
A pure state is separable iff the partial trace on the left is pure.
Source project: quantumInfo
Person-level attribution pending.
MState.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.