Multi Tau min sum le
multiTau_min_sum_le
Plain-language statement
If is a -minimizer, then .
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
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 160 research declarations. Search 10,000 more complete Mathlib declarations.
160 results
Clear filtersmultiTau_min_sum_le
Plain-language statement
If is a -minimizer, then .
Source project: Polynomial Freiman-Ruzsa project
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.