OAI/NumberTheory/Jacobsthal/Primes/PrimeCompactWeights.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.WeightedPrimeBins.weightedPrimeBin line 16
  2. theorem OAI.Erdos970.NumberTheoryLean.WeightedPrimeBins.weightedPrimeBin_sandwich line 19
  3. theorem OAI.Erdos970.NumberTheoryLean.WeightedPrimeBins.sandwich_difference line 45
  4. theorem OAI.Erdos970.NumberTheoryLean.WeightedPrimeBins.sub_le_mul_log_sub line 57
  5. theorem OAI.Erdos970.NumberTheoryLean.WeightedPrimeBins.multiplier_drop line 66
  6. theorem OAI.Erdos970.NumberTheoryLean.WeightedPrimeBins.weighted_bin_error line 79
  7. theorem OAI.Erdos970.NumberTheoryLean.WeightedPrimeBins.weighted_bin_polynomial_error line 95
  8. theorem OAI.Erdos970.NumberTheoryLean.NormalizedPrimeBins.division_error line 162
  9. def OAI.Erdos970.NumberTheoryLean.NormalizedPrimeBins.normalizedPrimeBin line 176
  10. theorem OAI.Erdos970.NumberTheoryLean.NormalizedPrimeBins.normalizedPrimeBin_eq line 179
  11. theorem OAI.Erdos970.NumberTheoryLean.NormalizedPrimeBins.normalized_bin_error line 183
  12. def OAI.Erdos970.NumberTheoryLean.PrimeBinMembership.Consistent line 209
  13. theorem OAI.Erdos970.NumberTheoryLean.PrimeBinMembership.step_consistent line 211
  14. theorem OAI.Erdos970.NumberTheoryLean.PrimeBinMembership.terminal_consistent line 219
  15. theorem OAI.Erdos970.NumberTheoryLean.PrimeBinMembership.history_consistent line 228
  16. theorem OAI.Erdos970.NumberTheoryLean.PrimeBinMembership.children_full_bin line 233
  17. theorem OAI.Erdos970.NumberTheoryLean.PrimeBinMembership.normalized_children_full_bin line 280
  18. def OAI.Erdos970.NumberTheoryLean.ActualPrimeBins.liveBin line 305
  19. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeBins.mem_liveBin_some line 310
  20. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeBins.not_mem_liveBin_none line 313
  21. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeBins.liveBin_measurable line 318
  22. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeBins.chain_live_bin_formula line 320
  23. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeBins.chain_full_bin line 331
  24. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeBins.chain_full_bin_real line 356
  25. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.allowed_prime_bounds line 383
  26. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.allowed_decreasing line 402
  27. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.allowed_mem_decreasing line 413
  28. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.terminal_gap_remaining line 431
  29. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.terminal_cutoff line 440
  30. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.terminal_ratio_remaining line 446
  31. def OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.actualHasHigh line 458
  32. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.actual_has_high_iff line 461
  33. def OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.uncappedChildren line 484
  34. def OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.uncappedAllowed line 490
  35. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.allowed_mono line 494
  36. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.uncapped_iff_exists_ceiling line 505
  37. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.uncapped_mem_decreasing line 527
  38. def OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.uncappedPrefixes line 533
  39. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.mem_uncappedPrefixes line 537
  40. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.uncapped_gap_positive line 543
  41. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.uncapped_has_high_iff line 549
  42. def OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.uncappedLowGapHighMass line 568
  43. def OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.uncappedRewardedHighMass line 573
  44. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.uncapped_reward_filter line 578
  45. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.uncapped_low_mass_le line 592
  46. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeHigh.uncapped_rewarded_mass_le line 609
  47. def OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.retainedPrefixes line 639
  48. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.mem_retainedPrefixes line 643
  49. def OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.retainedHistoryEquiv line 655
  50. abbrev OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.historyFintype line 662
  51. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.sum_histories line 666
  52. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.retained_history_horizon line 677
  53. def OAI.Erdos970.NumberTheoryLean.PrimeCompactWeights.inverseBound line 699
  54. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactWeights.valid_compact_end line 701
  55. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactWeights.inverseBound_pos line 704
  56. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactWeights.compact_inverse_weight line 707
  57. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactWeights.terminal_cutoff_lower line 716
  58. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactWeights.history_ratio_le_gap line 727
  59. def OAI.Erdos970.NumberTheoryLean.PrimeCompactWeights.compactConstant line 738
  60. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactWeights.compactConstant_pos line 741
  61. def OAI.Erdos970.NumberTheoryLean.PrimeCompactWeights.scaledWeight line 747
  62. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactWeights.scaledWeight_nonneg line 752
  63. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactWeights.scaled_compact_bound line 763