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 filtersArkLib.Lattices.CyclotomicModulus.Rq.l1Norm_one
Plain-language statement
The centered ℓ₁ norm of 1 : Rq Φ is 1 (when 1 ≤ deg φ): the trivial challenge c = 1 used by the honest committer is nonzero and ℓ₁-short.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.Rq.l2NormSq_le_natDegree_mul_lInftyNorm_sq
Plain-language statement
ℓ∞ → ℓ₂² bridge (ring element): ‖x‖₂² ≤ deg φ · ‖x‖∞² , each of the deg φ centered coefficients contributes at most ‖x‖∞².
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.Rq.l2NormSq_mul_le
Plain-language statement
Per-entry product norm bound (Micciancio/Young, cf. [Mic07, ineqs. (2.6)–(2.7)]). Over the negacyclic ring X^{2^α}+1, ‖d·w‖₂² ≤ ‖d‖₁²·‖w‖₂².
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.Rq.l2NormSq_sub_le
Plain-language statement
Per-element subtraction bound: ‖a - b‖₂² ≤ 2·(‖a‖₂² + ‖b‖₂²).
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.Rq.lInftyNorm_sub_le
Plain-language statement
Per-element ℓ∞ triangle inequality: ‖a - b‖∞ ≤ ‖a‖∞ + ‖b‖∞.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.scalarVecMul_mul_l2NormSq_le
Plain-language statement
Micciancio/Young product bound. Over the power-of-two cyclotomic modulus powTwoCyclotomic α (φ = X^{2^α}+1), scaling an already-c-scaled vector by a further ring element d of bounded centered ℓ₁ norm grows the squared ℓ₂ norm by at most κ² (the honest Young/Micciancio inequality ‖(c·d)·v‖₂² ≤ ‖d‖₁² · ‖c·v‖₂² over the negacyclic convolu...
Source project: ArkLib
Person-level attribution pending.