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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,801 to 1,806 of 2,569 results.
OptimalHypothesisRate.iInf_IsCompact
Mathematical statement
The space of strategies T in OptimalHypothesisRate is compact.
Source project: quantumInfo
Person-level attribution pending.
OptimalHypothesisRate.iInf_IsConvex
Mathematical statement
The space of strategies T in OptimalHypothesisRate is convex.
Source project: quantumInfo
Person-level attribution pending.
OptimalHypothesisRate.optimalHypothesisRate_unique
Mathematical 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 ρ=σ.) -
Source project: quantumInfo
Person-level attribution pending.
OptimalHypothesisRate.pos_of_lt_one
Mathematical 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.
Source project: quantumInfo
Person-level attribution pending.
Oracle.fold_succ_prob
Mathematical statement
(o.fold (n+1)).prob y decomposes as a product
Source project: debate
Person-level attribution pending.
OracleComp.bind_congr_of_forall_mem_support
Mathematical statement
Support-aware bind congruence: if two continuations agree on all elements in the support of mx, the resulting bind computations are equal.
Source project: VCVio
Person-level attribution pending.