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,447 to 1,452 of 2,569 results.
JohnsonBound.johnson_condition_weak_implies_strong
Mathematical statement
The weak Johnson condition implies the strong one on the ball intersection.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.johnson_d_le_n
Mathematical statement
The average pairwise distance d(B) is at most n.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.johnson_den_lb_e_pos
Mathematical statement
Lower bound on the Johnson denominator when e > 0.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.johnson_denom
Mathematical statement
Algebraic identity expressing the Johnson LHS as a difference of squares.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.johnson_e_div_ne_J
Mathematical statement
The ratio e/n cannot equal J'(q, d/n) under the Johnson hypothesis.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.johnson_gap_frac_d_gt_one
Mathematical statement
When q · d / ((q-1) · n) > 1, there is a positive gap of size ≥ 1/((q-1)·n).
Source project: ArkLib
Person-level attribution pending.