OAI/NumberTheory/JointDickman/Amplification/LargeCardinalityPartition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Partitioning all large high-endpoint alternatives by cardinality

  1. def OAI.JointDickman.allLargeHighAlternativePairs line 10
  2. theorem OAI.JointDickman.allLargeHighAlternativePairs_fiber line 21
  3. theorem OAI.JointDickman.regular_addition_card_le_logLength line 30
  4. theorem OAI.JointDickman.allLargeHighAlternativePairs_card line 45