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 filtersMState.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.
operator_ineq_SSA
Plain-language statement
Operator extension of SSA (Main result of Lin-Kim-Hsieh). For positive definite ρ_AB and σ_BC: ρ_A⁻¹ ⊗ σ_BC ≤ ρ_AB⁻¹ ⊗ σ_C where ρ_A = Tr_B(ρ_AB) and σ_C = Tr_B(σ_BC), and the RHS is reindexed via the associator (dA × dB) × dC ≃ dA × (dB × dC).
Source project: quantumInfo
Person-level attribution pending.
OptimalHypothesisRate.exists_min
Plain-language statement
There exists an optimal T for the hypothesis testing, that is, it's a minimum and not just an infimum. This tightens the T from exists_min' to a ⟪ρ,T⟫ = 1 - ε bound.
Source project: quantumInfo
Person-level attribution pending.
OptimalHypothesisRate.exists_min'
Plain-language statement
There exists an optimal T for the hypothesis testing, that is, it's a minimum and not just an infimum. This states we have 1 - ε ≤ ρ.exp_val T, but we can always "worsen" T to make that bound tight, which is exists_min.
Source project: quantumInfo
Person-level attribution pending.
OptimalHypothesisRate.iInf_IsCompact
Plain-language statement
The space of strategies T in OptimalHypothesisRate is compact.
Source project: quantumInfo
Person-level attribution pending.
OptimalHypothesisRate.iInf_IsConvex
Plain-language statement
The space of strategies T in OptimalHypothesisRate is convex.
Source project: quantumInfo
Person-level attribution pending.