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 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersArkLib.Lattices.CyclotomicModulus.sub_lInftyNorm_le
Plain-language statement
ℓ∞ subtraction bound. The ℓ∞ norm of a difference of two vectors, each within bound, is within subLInftyNormBound bound = 2·bound.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.valMinAbs_natAbs_le
Plain-language statement
The centered representative valMinAbs has the least absolute value among all integer representatives of a residue class.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.vecL2NormSq_le_card_mul_lInftyNorm_sq
Plain-language statement
ℓ∞ → ℓ₂² bridge (vector): ‖v‖₂² ≤ cols · (deg φ · ‖v‖∞²).
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.vecLInftyNorm_flattenBlocks_le
Plain-language statement
The ℓ∞ norm of a flattened block vector is bounded by γ as soon as every block is: the ℓ∞ norm of flattenBlocks is the supremum of the per-block ℓ∞ norms.
Source project: ArkLib
Person-level attribution pending.
Automata.na_AcceptedLang_of_FinAccept'
Project documentation
The following theorem shows that under the assumption that the alphabet type A is inhabited, the definitions using infinite sequences and those using finite sequences actually define the same notion of the accepted language of an automaton.
Source project: Automata Theory
Person-level attribution pending.
Binius.BinaryBasefold.toOutCodewordsCount_mul_ϑ_eq_i_succ
Plain-language statement
If a new oracle is committed at round i + 1 (i.e., ϑ ∣ i + 1), then the index of this new oracle (which is the count of oracles from the previous round, i) multiplied by ϑ equals the current round number i + 1. TODO: double check why this is still correct when replacing hCR with ϑ | i + 1
Source project: ArkLib
Person-level attribution pending.