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

Optimal Hypothesis Rate unique

OptimalHypothesisRate.optimalHypothesisRate_unique

Plain-language statement

On the 1D Hilbert space, the optimal hypothesis testing rate is simply 1 - ε, since there's nothing to learn. (More generally this would hold whenever ρ=σ.) -

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record
Project-declaredLean 4.28.0

Pos of lt one

OptimalHypothesisRate.pos_of_lt_one

Plain-language statement

When the allowed Type I error ε is less than 1 (so, we have some limit on our errors), and the kernel of the state ρ contains the kernel of some element in S, then the optimal hypothesis rate is positive - there is some lower bound on the type II errors we'll see. In other words, under these conditions, we cannot completely avoid type II errors.

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

PFR conjecture

PFR_conjecture

Plain-language statement

The polynomial Freiman-Ruzsa (PFR) conjecture: if A is a subset of an elementary abelian 2-group of doubling constant at most K, then A can be covered by at most 2 * K ^ 12 cosets of a subgroup of cardinality at most |A|.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

PFR conjecture improv

PFR_conjecture_improv

Project documentation

Improved polynomial Freiman-Ruzsa theorem. Let AA be a nonempty subset of a finite elementary abelian 22-group. If A+AKA|A+A|\le K|A|, then there are a subspace HH and a set of representatives cc such that Ac+HA\subseteq c+H, c<2K11|c|<2K^{11}, and HA|H|\le|A|.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

PFR conjecture improv

PFR_conjecture_improv'

Project documentation

Improved polynomial Freiman-Ruzsa theorem without a finite ambient-group assumption. Let AA be a nonempty finite subset of an elementary abelian 22-group. If A+AKA|A+A|\le K|A|, then there are a finite subspace HH and a finite set cc such that Ac+HA\subseteq c+H, c<2K11|c|<2K^{11}, and HA|H|\le|A|.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

PFR conjecture

PFR_conjecture'

Project documentation

Polynomial Freiman-Ruzsa theorem without a finite ambient-group assumption. Let AA be a nonempty finite subset of an elementary abelian 22-group. If A+AKA|A+A|\le K|A|, then there are a finite subspace HH and a finite set cc such that Ac+HA\subseteq c+H, c<2K12|c|<2K^{12}, and HA|H|\le|A|.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record