OAI/NumberTheory/PowerFree/AdaptiveFibres.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.card_image_le_mul_fibers line 18
  2. def OAI.QuarticPowerFree.adaptiveStateAt line 35
  3. theorem OAI.QuarticPowerFree.adaptiveStateAt_tail line 43
  4. theorem OAI.QuarticPowerFree.adaptiveStateAt_mem_states line 54
  5. def OAI.QuarticPowerFree.physicalStateAt line 70
  6. theorem OAI.QuarticPowerFree.physicalStateAt_zero line 76
  7. theorem OAI.QuarticPowerFree.physicalStateAt_succ line 80
  8. theorem OAI.QuarticPowerFree.physicalStateAt_good line 88
  9. def OAI.QuarticPowerFree.pastBlockPrimes line 99
  10. theorem OAI.QuarticPowerFree.pastBlockPrimes_zero line 102
  11. theorem OAI.QuarticPowerFree.pastBlockPrimes_succ line 105
  12. theorem OAI.QuarticPowerFree.cumulativeBlockPrimes_eq_union line 109
  13. theorem OAI.QuarticPowerFree.residueTuple_cumulative_eq line 126
  14. def OAI.QuarticPowerFree.physicalNode line 137
  15. theorem OAI.QuarticPowerFree.physical_fixed_residue_children line 144
  16. theorem OAI.QuarticPowerFree.physical_node_branch_bound line 198
  17. def OAI.QuarticPowerFree.activePoints line 269
  18. theorem OAI.QuarticPowerFree.activePoints_succ_subset line 272
  19. theorem OAI.QuarticPowerFree.active_node_count line 278
  20. theorem OAI.QuarticPowerFree.active_stopping_count line 297
  21. theorem OAI.QuarticPowerFree.physical_initial_node_count line 324