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 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersProver.liftContext_processRound
Plain-language statement
Lifting the prover intertwines with the process round function
Source project: ArkLib
Person-level attribution pending.
ProximityGap.exists_large_of_finset_cover
Plain-language statement
Pigeonhole for finite covers: if U is covered by L indexed subsets and L * B < |U|, then some subset has more than B elements.
Source project: ArkLib
Person-level attribution pending.
ProximityGap.exists_Pz_of_coeffs_of_close_proximity
Plain-language statement
There exists a δ-close polynomial P_z for each z from the set S.
Source project: ArkLib
Person-level attribution pending.
ProximityGap.folded_rate_eq
Plain-language statement
The rate of the folded RS-code is the same.
Source project: ArkLib
Person-level attribution pending.
ProximityGap.folding_preserves_distance
Plain-language statement
Folding preserves distance from Reed–Solomon codes. For any word f over the smooth coset FFT domain, degree parameter d, folding parameter k, and distance threshold δ satisfying 0 < δ < min (δᵣ(f, RS[d])) (1 - sqrtRate(d)), the probability over a uniformly random folding challenge r : F that the folded word is within relative distance δ of t...
Source project: ArkLib
Person-level attribution pending.
ProximityGap.foldWord_k_1_of_sq_roots
Plain-language statement
An explicit formula for foldWord when k = 1 that does not use Lagrange interpolation and avoids using log.
Source project: ArkLib
Person-level attribution pending.