OAI/Combinatorics/CompleteCrossing/LowerBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial injectivity and the lower bound on crossing-tensor support.

  1. theorem OAI.Paper170.kernel_diagonal_vanishing line 30
  2. theorem OAI.Paper170.kernel_collision_divisibility line 36
  3. theorem OAI.Paper170.support_evaluation_injective line 41
  4. theorem OAI.Paper170.support_cardinality_lower_bound line 46