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 27 research declarations. Search 10,000 more complete Mathlib declarations.
27 results
Clear filterstraceFunctional_eq_iSup_f_alpha
Plain-language statement
Step 1 (Variational formula): For α > 1, the trace functional equals the supremum of f_α over all PSD H: Q̃_α(ρ‖σ) = ⨆ (H : HermitianMat d ℂ) (_ : 0 ≤ H), f_alpha α H ρ σ. The optimizer is H_hat = σ^γ (σ^γ ρ σ^γ)^{α−1} σ^γ.
Source project: quantumInfo
Person-level attribution pending.
twirling_general_matrix
Project documentation
The trace functional is invariant under 1_A ⊗ V conjugation. -/ theorem sandwichedTraceFunctional_conj_tensorUnitary (ρ σ : MState (dA × dB)) (V : Matrix.unitaryGroup dB ℂ) : Q̃_ α(ρ.conjTensorUnitary V‖σ.conjTensorUnitary V) = Q̃_ α(ρ‖σ) := by exact sandwichedTraceFunctional_conj_unitary_MState _ ρ σ section twirling variable {dA dB : Type*} variable [...
Source project: quantumInfo
Person-level attribution pending.
twirling_hermitian_entry
Project documentation
The trace functional is invariant under 1_A ⊗ V conjugation. -/ theorem sandwichedTraceFunctional_conj_tensorUnitary (ρ σ : MState (dA × dB)) (V : Matrix.unitaryGroup dB ℂ) : Q̃_ α(ρ.conjTensorUnitary V‖σ.conjTensorUnitary V) = Q̃_ α(ρ‖σ) := by exact sandwichedTraceFunctional_conj_unitary_MState _ ρ σ section twirling variable {dA dB : Type*} variable [...
Source project: quantumInfo
Person-level attribution pending.