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 160 research declarations. Search 10,000 more complete Mathlib declarations.
160 results
Clear filtersMState.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.
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.
multiDist_of_cast
Plain-language statement
Multidistance is unchanged when a finite family of random variables is reindexed along an equality . This says that the quantity depends on the family, not on the particular equal presentation of its finite index type.
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
multidist_ruzsa_IV
Project documentation
Let m ≥ 2, and let X_[m] be a tuple of G-valued random variables. Let W := ∑ X_i. Then d[W;-W] ≤ 2 D[X_i].
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.