OAI/Combinatorics/Progressions/Dynamics/SquarefreeModelBudget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.squarefreeBracketHeight_le_exp line 11
  2. theorem OAI.Erdos3.squarefreeStructureHeight_le_exp line 26
  3. def OAI.Erdos3.squarefreeInputBudget line 52
  4. def OAI.Erdos3.squarefreeModelBudget line 54
  5. theorem OAI.Erdos3.squarefreeInputBudget_nonneg line 59
  6. theorem OAI.Erdos3.le_squarefreeInputBudget line 64
  7. theorem OAI.Erdos3.squarefreeInputBudget_le_model line 69
  8. theorem OAI.Erdos3.squarefreeStructureHeight_ceil_exp line 74
  9. theorem OAI.Erdos3.squarefree_grid_budget line 81