OAI/NumberTheory/SiegelZeros/Selection/EventuallyPivots.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.W32.count_lt_le line 19
  2. theorem OAI.SiegelZeros.WeightedTorusJets.W32.pair_count_identity line 31
  3. theorem OAI.SiegelZeros.WeightedTorusJets.W32.occupancy_nat line 50
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W32.occupancy_real line 67
  5. def OAI.SiegelZeros.Result.Workers.W33.occupancyCap line 89
  6. theorem OAI.SiegelZeros.Result.Workers.W33.occupancyCap_pos line 91
  7. theorem OAI.SiegelZeros.Result.Workers.W33.occupancyCap_le line 95
  8. theorem OAI.SiegelZeros.Result.Workers.W33.occupancy_lower_strengthen line 104
  9. theorem OAI.SiegelZeros.Result.Workers.W33.negative_third_squared line 118
  10. theorem OAI.SiegelZeros.Result.Workers.W33.negative_two_thirds_cancel line 124
  11. theorem OAI.SiegelZeros.Result.Workers.W33.negative_third_mul_self line 129
  12. theorem OAI.SiegelZeros.Result.Workers.W33.source_scale_ge_one line 136
  13. theorem OAI.SiegelZeros.Result.Workers.W33.source_occupancyCap_le line 148
  14. theorem OAI.SiegelZeros.Result.Workers.W33.source_dimension line 155
  15. theorem OAI.SiegelZeros.Result.Workers.W33.source_twice_occupancyCap_le line 160
  16. theorem OAI.SiegelZeros.Result.Workers.W33.eventually_twice_occupancyCap_le line 180
  17. theorem OAI.SiegelZeros.Result.Workers.W33.source_pivot_lower line 190
  18. theorem OAI.SiegelZeros.Result.Workers.W33.pivot_ratio line 218
  19. theorem OAI.SiegelZeros.Result.Workers.W33.finite_pivot_lower line 245
  20. theorem OAI.SiegelZeros.Result.Workers.W33.cutoff_pivot_lower line 259
  21. theorem OAI.SiegelZeros.Result.Workers.W33.cutoff_pivot_ratio line 270
  22. theorem OAI.SiegelZeros.Result.Workers.W33.cutoff_pivot_ratio_le_twelfth line 283
  23. def OAI.SiegelZeros.Result.Workers.W33.firstOrder line 308
  24. def OAI.SiegelZeros.Result.Workers.W33.transverseOrder line 311
  25. theorem OAI.SiegelZeros.Result.Workers.W33.eventual_pivot_bounds line 314
  26. theorem OAI.SiegelZeros.Result.Workers.W33.eventual_pivot_ratio_le_twelfth line 347
  27. theorem OAI.SiegelZeros.Result.Workers.W33.exists_fixed_weight line 364