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 6 research declarations. Search 10,000 more complete Mathlib declarations.
6 results
Clear filtersconvex_roof_of_pure
Plain-language statement
The convex roof extension of g : KetUpToPhase d → ℝ≥0 applied to a pure state ψ is g (KetUpToPhase.mk ψ).
Source project: quantumInfo
Person-level attribution pending.
EoF_of_MES
Plain-language statement
The entanglement of formation of the maximally entangled state with on-site dimension 𝕕 is log(𝕕).
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.
Sᵥₙ_eq_trace_cfc
Plain-language statement
Entanglement of Formation of bipartite systems. It is the convex roof extension of the von Neumann entropy of one of the subsystems (here chosen to be the left one, but see Entropy.Sᵥₙ_of_partial_eq). The function Sᵥₙ ∘ traceRight ∘ pure is phase-invariant because pure maps phase-equivalent kets to the same mixed state, so it descends to `KetUpToPha...
Source project: quantumInfo
Person-level attribution pending.
Sᵥₙ_ofClassical
Plain-language statement
Entanglement of Formation of bipartite systems. It is the convex roof extension of the von Neumann entropy of one of the subsystems (here chosen to be the left one, but see Entropy.Sᵥₙ_of_partial_eq). The function Sᵥₙ ∘ traceRight ∘ pure is phase-invariant because pure maps phase-equivalent kets to the same mixed state, so it descends to `KetUpToPha...
Source project: quantumInfo
Person-level attribution pending.
traceRight_pure_MES
Plain-language statement
Entanglement of Formation of bipartite systems. It is the convex roof extension of the von Neumann entropy of one of the subsystems (here chosen to be the left one, but see Entropy.Sᵥₙ_of_partial_eq). The function Sᵥₙ ∘ traceRight ∘ pure is phase-invariant because pure maps phase-equivalent kets to the same mixed state, so it descends to `KetUpToPha...
Source project: quantumInfo
Person-level attribution pending.