Project-declaredLean 4.28.0
Lb theorem
SupRegularized.lb
Plain-language statement
The SupRegularized value is also lower bounded.
quantum informationentropyquantum channels
Source project: quantumInfo
Person-level attribution pending.
Source-pinned research
Research proof index
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 filtersView proof record
Project-declaredLean 4.28.0
Mono sup
SupRegularized.mono_sup
Plain-language statement
For Monotone functions, the SupRegularized is the supremum of values.
quantum informationentropyquantum channels
Source project: quantumInfo
Person-level attribution pending.
Project-declaredLean 4.28.0
Sᵥₙ eq trace cfc
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...
quantum informationentropyquantum channels
Source project: quantumInfo
Person-level attribution pending.
Project-declaredLean 4.28.0
Sᵥₙ of Classical
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...
quantum informationentropyquantum channels
Source project: quantumInfo
Person-level attribution pending.
Project-declaredLean 4.28.0
Sᵥₙ pure tripartite triangle
Sᵥₙ_pure_tripartite_triangle
Plain-language statement
Triangle inequality for pure tripartite states: S(A) ≤ S(B) + S(C).
quantum informationentropyquantum channels
Source project: quantumInfo
Person-level attribution pending.
Project-declaredLean 4.28.0
Sᵥₙ strong subadditivity
Sᵥₙ_strong_subadditivity
Plain-language statement
Strong subadditivity on a tripartite system
quantum informationentropyquantum channels
Source project: quantumInfo
Person-level attribution pending.