OAI/NumberTheory/SiegelZeros/Estimates/AsymptoticAssembly.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.W48.auxiliaryN line 19
  2. def OAI.SiegelZeros.WeightedTorusJets.W48.auxiliaryU line 21
  3. theorem OAI.SiegelZeros.WeightedTorusJets.W48.N_real_tendsto_atTop line 24
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W48.N_nat_tendsto_atTop line 28
  5. theorem OAI.SiegelZeros.WeightedTorusJets.W48.U_tendsto_atTop line 32
  6. theorem OAI.SiegelZeros.WeightedTorusJets.W48.log_U_tendsto_atTop line 37
  7. theorem OAI.SiegelZeros.WeightedTorusJets.W48.auxiliaryN_pos line 41
  8. theorem OAI.SiegelZeros.WeightedTorusJets.W48.log_N_bounds line 45
  9. theorem OAI.SiegelZeros.WeightedTorusJets.W48.log_N_div_log_tendsto line 62
  10. theorem OAI.SiegelZeros.WeightedTorusJets.W48.log_U_div_log_tendsto line 79
  11. theorem OAI.SiegelZeros.WeightedTorusJets.W48.eventually_N_ge line 91
  12. theorem OAI.SiegelZeros.WeightedTorusJets.W48.log_div_log_U_tendsto line 95
  13. theorem OAI.SiegelZeros.WeightedTorusJets.W48.natural_conductor_limits line 101
  14. theorem OAI.SiegelZeros.W49.count_error_bound line 121
  15. theorem OAI.SiegelZeros.W49.entropy_error_bound line 133
  16. theorem OAI.SiegelZeros.W49.delta_error_tendsto line 149
  17. theorem OAI.SiegelZeros.W49.fixed_error_tendsto line 156
  18. theorem OAI.SiegelZeros.W49.count_error_tendsto line 174
  19. theorem OAI.SiegelZeros.W49.entropy_error_tendsto line 191
  20. theorem OAI.SiegelZeros.W49.determinant_error_tendsto line 210
  21. theorem OAI.SiegelZeros.W49.log_volume_identity line 229
  22. theorem OAI.SiegelZeros.SiegelZerosAwei.W50.false_of_master_and_pivot_estimates line 245
  23. theorem OAI.SiegelZeros.SiegelZerosAwei.W50.false_of_ceiling_master line 278