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 filtersMicroHamiltonian.entropy_A_eq_entropy_Z
Plain-language statement
The two definitions of entropy, in terms of T or β, are equivalent.
Source project: quantumInfo
Person-level attribution pending.
mixed_convex_roof_of_pure
Plain-language statement
The mixed convex roof extension of f : MState d → ℝ≥0 applied to a pure state ψ is f (pure ψ).
Source project: quantumInfo
Person-level attribution pending.
MState.fidelity_self_eq_one
Plain-language statement
A state has perfect fidelity with itself.
Source project: quantumInfo
Person-level attribution pending.
MState.Ket.IsProd_iff_rank_eq_one
Plain-language statement
A ket on a product space is a product state if and only if its coefficient matrix has rank 1.
Source project: quantumInfo
Person-level attribution pending.
MState.multiset_spectrum_relabel_eq
Plain-language statement
The multiset of values in the spectrum of a relabeled state is the same as the multiset of values in the spectrum of the original state.
Source project: quantumInfo
Person-level attribution pending.
MState.no_cloning
Project documentation
The No-cloning theorem, saying that if states ψ and φ can both be perfectly cloned using a unitary U and a fiducial state f, and they aren't identical (their inner product is less than 1), then the two states must be orthogonal to begin with. In short: only orthogonal states can be simultaneously cloned.
Source project: quantumInfo
Person-level attribution pending.