OAI/NumberTheory/Jacobsthal/Estimates/SmallModelSourceScales.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosInverseFrozen.frozenCoordinates line 19
  2. theorem OAI.Erdos970.ErdosInverseFrozen.mem_frozenCoordinates line 23
  3. theorem OAI.Erdos970.ErdosInverseFrozen.frozenCoordinates_eq_of_modEq line 33
  4. def OAI.Erdos970.ErdosInverseEuler.smallModulus line 60
  5. theorem OAI.Erdos970.ErdosInverseEuler.smallModulus_pos line 62
  6. theorem OAI.Erdos970.ErdosInverseEuler.log_smallModulus_eq_theta line 66
  7. theorem OAI.Erdos970.ErdosInverseEuler.log_smallModulus_le line 74
  8. theorem OAI.Erdos970.ErdosInverseEuler.smallModulus_le_exp line 79
  9. theorem OAI.Erdos970.ErdosInverseFrozen.cutoffPrime_dvd_smallModulus line 95
  10. theorem OAI.Erdos970.ErdosInverseFrozen.parentCoordinates_eq_pattern line 100
  11. theorem OAI.Erdos970.ErdosInverseFrozen.parentCoordinates_eq_frozen_center line 122
  12. theorem OAI.Erdos970.ErdosInverseFrozen.actual_parent_count_frozen line 134
  13. theorem OAI.Erdos970.ErdosInverseFrozen.actual_child_count_frozen line 145
  14. def OAI.Erdos970.ErdosVarianceSmallModel.divisorPrimes line 170
  15. def OAI.Erdos970.ErdosVarianceSmallModel.coprimePrimes line 172
  16. def OAI.Erdos970.ErdosVarianceSmallModel.divisorModulus line 174
  17. def OAI.Erdos970.ErdosVarianceSmallModel.coprimeModulus line 175
  18. theorem OAI.Erdos970.ErdosVarianceSmallModel.divisorModulus_pos line 177
  19. theorem OAI.Erdos970.ErdosVarianceSmallModel.coprimeModulus_pos line 180
  20. theorem OAI.Erdos970.ErdosVarianceSmallModel.pattern_moduli_product line 183
  21. theorem OAI.Erdos970.ErdosVarianceSmallModel.divisorModulus_dvd_H line 189
  22. theorem OAI.Erdos970.ErdosVarianceSmallModel.coprimeModulus_coprime_H line 196
  23. theorem OAI.Erdos970.ErdosVarianceSmallModel.pattern_moduli_coprime line 202
  24. theorem OAI.Erdos970.ErdosVarianceSmallModel.effective_pattern_coprime line 205
  25. theorem OAI.Erdos970.ErdosVarianceSmallModel.pattern_totient line 209
  26. theorem OAI.Erdos970.ErdosVarianceSmallModel.pattern_modulus_size line 216
  27. theorem OAI.Erdos970.ErdosVarianceSmallModel.prime_coprime_small_pattern line 220
  28. theorem OAI.Erdos970.ErdosInverseEuler.sourceW_tendsto_atTop line 242
  29. theorem OAI.Erdos970.ErdosInverseEuler.sourceZ_le_rpow line 259
  30. theorem OAI.Erdos970.ErdosInverseEuler.smallModulus_source_power line 273
  31. instance OAI.Erdos970.ErdosVarianceSmallModel.(instance at line 304) line 304
  32. instance OAI.Erdos970.ErdosVarianceSmallModel.(instance at line 305) line 305
  33. abbrev OAI.Erdos970.ErdosVarianceSmallModel.Pattern line 307
  34. abbrev OAI.Erdos970.ErdosVarianceSmallModel.ModelPoint line 308
  35. theorem OAI.Erdos970.ErdosVarianceSmallModel.pattern_card line 310
  36. theorem OAI.Erdos970.ErdosInverseEuler.exp_loglog_sq_le_sourceZ line 326
  37. theorem OAI.Erdos970.ErdosInverseEuler.log_pow_le_sourceZ line 351
  38. theorem OAI.Erdos970.ErdosInverseEuler.sourceZ_tendsto_atTop line 368
  39. theorem OAI.Erdos970.ErdosInverseEuler.smallModulus_mul_log_power line 374
  40. theorem OAI.Erdos970.ErdosInverseTail.source_common_length_regime line 397
  41. theorem OAI.Erdos970.ErdosVarianceSmallModel.source_Z_power_R line 451
  42. theorem OAI.Erdos970.ErdosVarianceSmallModel.primeWidth_lower_Z line 468
  43. theorem OAI.Erdos970.ErdosVarianceSmallModel.source_prime_width_lower line 483
  44. theorem OAI.Erdos970.ErdosVarianceSmallModel.source_small_modulus_R line 505