OAI/NumberTheory/Jacobsthal/Partitions/CrossingBandGeometry.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.LogarithmicBinScale.binCount line 14
  2. def OAI.Erdos970.NumberTheoryLean.LogarithmicBinScale.logWidth line 15
  3. def OAI.Erdos970.NumberTheoryLean.LogarithmicBinScale.effectiveWidth line 16
  4. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinScale.span_log_pos line 18
  5. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinScale.binCount_pos line 22
  6. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinScale.logWidth_pos line 26
  7. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinScale.count_mul_logWidth line 30
  8. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinScale.logWidth_le line 36
  9. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinScale.logWidth_ge_half line 45
  10. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinScale.effectiveWidth_pos line 59
  11. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinScale.effectiveWidth_le line 63
  12. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinScale.effectiveWidth_ge_quarter line 69
  13. def OAI.Erdos970.NumberTheoryLean.LogarithmicBinEndpoints.endpoint line 90
  14. def OAI.Erdos970.NumberTheoryLean.LogarithmicBinEndpoints.lower line 91
  15. def OAI.Erdos970.NumberTheoryLean.LogarithmicBinEndpoints.width line 92
  16. def OAI.Erdos970.NumberTheoryLean.LogarithmicBinEndpoints.upper line 93
  17. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinEndpoints.endpoint_zero line 96
  18. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinEndpoints.upper_endpoint line 98
  19. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinEndpoints.endpoint_count line 103
  20. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinEndpoints.endpoint_pos line 108
  21. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinEndpoints.endpoint_mono line 111
  22. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinEndpoints.bin_source_bounds line 117
  23. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinEndpoints.bins_separated line 132
  24. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinEndpoints.last_bin_endpoint line 144
  25. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinEndpoints.bin_prime_in_source line 148
  26. def OAI.Erdos970.NumberTheoryLean.LogarithmicBinLabels.coordinate line 163
  27. def OAI.Erdos970.NumberTheoryLean.LogarithmicBinLabels.index line 165
  28. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinLabels.coordinate_bounds line 168
  29. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinLabels.index_lt line 180
  30. def OAI.Erdos970.NumberTheoryLean.LogarithmicBinLabels.label line 186
  31. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinLabels.index_eq_ceiling line 189
  32. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinLabels.label_coordinate_bounds line 194
  33. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinLabels.label_value_bounds line 209
  34. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinLabels.label_prime_membership line 232
  35. def OAI.Erdos970.NumberTheoryLean.LogarithmicBinPartition.sourcePrimeSet line 247
  36. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinPartition.mem_sourcePrimeSet line 249
  37. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinPartition.bin_mem_iff_label line 264
  38. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinPartition.bins_pairwise_disjoint line 283
  39. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinPartition.union_bins_eq_source line 293
  40. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinPartition.source_sum_over_bins line 306
  41. theorem OAI.Erdos970.NumberTheoryLean.NearbyParentGeometry.minRatio_stability line 321
  42. theorem OAI.Erdos970.NumberTheoryLean.NearbyParentGeometry.log_stability line 329
  43. theorem OAI.Erdos970.NumberTheoryLean.NearbyParentGeometry.cost_stability line 344
  44. theorem OAI.Erdos970.NumberTheoryLean.NearbyParentGeometry.clipped_relative_stability line 359
  45. theorem OAI.Erdos970.NumberTheoryLean.NearbyParentGeometry.log_gap_relative line 366
  46. theorem OAI.Erdos970.NumberTheoryLean.NearbyParentGeometry.arrival_endpoint_stability line 374
  47. theorem OAI.Erdos970.NumberTheoryLean.NearbyParentGeometry.log_gap_step line 390
  48. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinMaps.source_list_boxed line 415
  49. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinMaps.source_representative_error line 422
  50. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinMaps.source_prefix_movement line 433
  51. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinMaps.common_width_bounds line 443
  52. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinMaps.endpoint_exponent line 452
  53. theorem OAI.Erdos970.NumberTheoryLean.LogarithmicBinMaps.representative_exponent line 458
  54. def OAI.Erdos970.NumberTheoryLean.IsolatedBinGeometry.isolatedBin line 474
  55. theorem OAI.Erdos970.NumberTheoryLean.IsolatedBinGeometry.source_left_error line 477
  56. theorem OAI.Erdos970.NumberTheoryLean.IsolatedBinGeometry.whole_bin_of_exponent_band line 497
  57. theorem OAI.Erdos970.NumberTheoryLean.IsolatedBinGeometry.isolated_bin_search line 507
  58. theorem OAI.Erdos970.NumberTheoryLean.RepeatedBinGeometry.equal_label_exponent_distance line 519
  59. theorem OAI.Erdos970.NumberTheoryLean.RepeatedBinGeometry.adjacent_ratio_slack line 532
  60. theorem OAI.Erdos970.NumberTheoryLean.RepeatedBinGeometry.matched_repeat_interval line 543
  61. theorem OAI.Erdos970.NumberTheoryLean.BinReplacementOrder.prime_order_replacement line 558
  62. theorem OAI.Erdos970.NumberTheoryLean.BinReplacementOrder.unique_label_other line 576
  63. theorem OAI.Erdos970.NumberTheoryLean.BinReplacementOrder.decreasing_replacement line 587
  64. theorem OAI.Erdos970.NumberTheoryLean.BinReplacementOrder.replacement_no_collision line 621
  65. def OAI.Erdos970.NumberTheoryLean.CrossingBandGeometry.crossingLower line 634
  66. def OAI.Erdos970.NumberTheoryLean.CrossingBandGeometry.crossingUpper line 635
  67. def OAI.Erdos970.NumberTheoryLean.CrossingBandGeometry.crossingWidth line 636
  68. def OAI.Erdos970.NumberTheoryLean.CrossingBandGeometry.crossingCenter line 637
  69. theorem OAI.Erdos970.NumberTheoryLean.CrossingBandGeometry.matched_gap_crossing line 639
  70. theorem OAI.Erdos970.NumberTheoryLean.CrossingBandGeometry.crossing_width_positive line 647
  71. theorem OAI.Erdos970.NumberTheoryLean.CrossingBandGeometry.crossing_cost_band line 649