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 44 research declarations. Search 10,000 more complete Mathlib declarations.
44 results
Clear filtersJohnsonBound.johnson_unrefined_by_M'
Plain-language statement
Johnson bound scaled by |F| / (|F| - 1).
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.johnson_worst_case_bound
Plain-language statement
Monotonicity of the worst-case Johnson quotient.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.k_choose_2
Plain-language statement
Jensen's inequality for choose_2 ∘ K at the zero coordinate.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.le_sum_choose_K
Plain-language statement
Lower bound on sum_choose_K_i via convexity.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.sum_choose_K'
Plain-language statement
Jensen's inequality applied to choose_2 for nonzero coordinates.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.sum_hamming_weight_sum
Plain-language statement
Sum of Hamming weights equals n · |B| minus total zero-coordinate counts.
Source project: ArkLib
Person-level attribution pending.