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.

1 topic

160 results

Clear filters
Project-declaredLean 4.33.0-rc1

Multi Tau min sum le

multiTau_min_sum_le

Plain-language statement

If (Xi)1im(X_i)_{1 \leq i \leq m} is a τ\tau-minimizer, then i=1md[Xi;X0]2mηd[X0;X0]\sum_{i=1}^m d[X_i; X^0] \leq \frac{2m}{\eta} d[X^0; X^0].

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.28.0

Operator ineq SSA

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).

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record
Project-declaredLean 4.28.0

Exists min

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.

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record
Project-declaredLean 4.28.0

Exists min

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.

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record
Project-declaredLean 4.28.0

I Inf Is Compact

OptimalHypothesisRate.iInf_IsCompact

Plain-language statement

The space of strategies T in OptimalHypothesisRate is compact.

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record
Project-declaredLean 4.28.0

I Inf Is Convex

OptimalHypothesisRate.iInf_IsConvex

Plain-language statement

The space of strategies T in OptimalHypothesisRate is convex.

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record