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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,453 to 1,458 of 2,569 results.
JohnsonBound.johnson_unrefined
Mathematical statement
Unrefined Johnson bound in terms of e, d, and |B|.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.johnson_unrefined_by_M'
Mathematical statement
Johnson bound scaled by |F| / (|F| - 1).
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.johnson_worst_case_bound
Mathematical statement
Monotonicity of the worst-case Johnson quotient.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.k_choose_2
Mathematical statement
Jensen's inequality for choose_2 ∘ K at the zero coordinate.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.le_sum_choose_K
Mathematical statement
Lower bound on sum_choose_K_i via convexity.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.sqrt_le_J
Mathematical statement
The binary Johnson bound 1 - √(1-δ) is at most the q-ary bound J q δ.
Source project: ArkLib
Person-level attribution pending.