Project-declaredLean 4.31.0
Le sum choose K
JohnsonBound.le_sum_choose_K
Plain-language statement
Lower bound on sum_choose_K_i via convexity.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
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 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersView proof record
Project-declaredLean 4.31.0
Sqrt le J
JohnsonBound.sqrt_le_J
Plain-language statement
The binary Johnson bound 1 - √(1-δ) is at most the q-ary bound J q δ.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Sum choose K
JohnsonBound.sum_choose_K'
Plain-language statement
Jensen's inequality applied to choose_2 for nonzero coordinates.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Sum hamming weight sum
JohnsonBound.sum_hamming_weight_sum
Plain-language statement
Sum of Hamming weights equals n · |B| minus total zero-coordinate counts.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Sum of not equals
JohnsonBound.sum_of_not_equals
Plain-language statement
Counting pairs that disagree at position i in terms of choose_2.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Sum sum K i eq n sub d
JohnsonBound.sum_sum_K_i_eq_n_sub_d
Plain-language statement
Total choose_2 over all coordinates equals choose_2(|B|) · (n - d).
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.