OAI/NumberTheory/Jacobsthal/Primes/PrimeRatioBins.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.PrimeTiltGeometry.childRatio line 17
  2. def OAI.Erdos970.NumberTheoryLean.PrimeTiltGeometry.capGuard line 19
  3. def OAI.Erdos970.NumberTheoryLean.PrimeTiltGeometry.children line 22
  4. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltGeometry.mem_children_iff line 27
  5. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltGeometry.child_valid line 46
  6. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltGeometry.child_exponent_positive line 52
  7. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltGeometry.nextExponent_childRatio line 57
  8. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltGeometry.nextGap_childRatio line 63
  9. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltGeometry.child_gap_positive line 69
  10. def OAI.Erdos970.NumberTheoryLean.PrimeTiltGeometry.primeTilt line 76
  11. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltGeometry.primeTilt_nonneg line 80
  12. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltGeometry.prime_tilt_step_identity line 86
  13. def OAI.Erdos970.NumberTheoryLean.PrimeTiltPrefixes.PrimeAdmissible line 109
  14. def OAI.Erdos970.NumberTheoryLean.PrimeTiltPrefixes.primeRatios line 114
  15. def OAI.Erdos970.NumberTheoryLean.PrimeTiltPrefixes.primeFinalGap line 118
  16. def OAI.Erdos970.NumberTheoryLean.PrimeTiltPrefixes.tiltProduct line 122
  17. def OAI.Erdos970.NumberTheoryLean.PrimeTiltPrefixes.normalizedTiltProduct line 126
  18. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltPrefixes.ratios_admissible line 131
  19. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltPrefixes.primeFinalGap_eq line 140
  20. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltPrefixes.primeFinalGap_pos line 152
  21. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltPrefixes.prime_prefix_weight_identity line 161
  22. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltPrefixes.normalized_product_correction line 184
  23. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltPrefixes.normalized_prime_prefix_weight_identity line 196
  24. def OAI.Erdos970.NumberTheoryLean.PrimeTiltBounds.multiplier line 215
  25. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltBounds.primeTilt_eq_multiplier line 218
  26. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltBounds.multiplier_pos line 223
  27. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltBounds.valid_ge_half line 228
  28. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltBounds.multiplier_envelope line 231
  29. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltBounds.log_lipschitz_half line 262
  30. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltBounds.log_multiplier line 281
  31. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltBounds.multiplier_log_lipschitz line 291
  32. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltBounds.multiplier_relative_bound line 323
  33. structure OAI.Erdos970.NumberTheoryLean.PrimeHistories.Node line 346
  34. def OAI.Erdos970.NumberTheoryLean.PrimeHistories.nodeChildren line 353
  35. def OAI.Erdos970.NumberTheoryLean.PrimeHistories.step line 356
  36. def OAI.Erdos970.NumberTheoryLean.PrimeHistories.terminal line 363
  37. def OAI.Erdos970.NumberTheoryLean.PrimeHistories.allowed line 365
  38. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.terminal_nil line 368
  39. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.terminal_cons line 369
  40. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.terminal_append line 372
  41. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.allowed_nil line 376
  42. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.allowed_cons line 378
  43. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.allowed_append line 381
  44. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.terminal_valid line 389
  45. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.terminal_gap_positive line 397
  46. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.terminal_ratio_le line 406
  47. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.terminal_gap_eq line 415
  48. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.terminal_ratio_eq line 421
  49. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.terminal_side_eq line 427
  50. structure OAI.Erdos970.NumberTheoryLean.PrimeHistories.History line 433
  51. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.History.ext line 441
  52. instance OAI.Erdos970.NumberTheoryLean.PrimeHistories.History.(instance at line 447) line 447
  53. instance OAI.Erdos970.NumberTheoryLean.PrimeHistories.History.(instance at line 448) line 448
  54. instance OAI.Erdos970.NumberTheoryLean.PrimeHistories.History.(instance at line 449) line 449
  55. def OAI.Erdos970.NumberTheoryLean.PrimeHistories.History.empty line 451
  56. def OAI.Erdos970.NumberTheoryLean.PrimeHistories.History.node line 452
  57. def OAI.Erdos970.NumberTheoryLean.PrimeHistories.History.append line 454
  58. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.History.append_primes line 459
  59. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistories.History.append_node line 462
  60. def OAI.Erdos970.NumberTheoryLean.PrimeRatioBins.ratioBin line 481
  61. def OAI.Erdos970.NumberTheoryLean.PrimeRatioBins.ratioBinMass line 486
  62. theorem OAI.Erdos970.NumberTheoryLean.PrimeRatioBins.ratio_interval_iff line 489
  63. theorem OAI.Erdos970.NumberTheoryLean.PrimeRatioBins.primeExponent_pos line 511
  64. theorem OAI.Erdos970.NumberTheoryLean.PrimeRatioBins.ratioBinMass_eq_harmonic line 517
  65. theorem OAI.Erdos970.NumberTheoryLean.PrimeRatioBins.bin_log_width line 527
  66. theorem OAI.Erdos970.NumberTheoryLean.PrimeRatioBins.bin_log_width_bounds line 532
  67. theorem OAI.Erdos970.NumberTheoryLean.PrimeRatioBins.prime_ratio_bin_error line 547