OAI/NumberTheory/Jacobsthal/Paths/WrongOwnerBoxMass.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.WrongOwnerBinMass.wrongOwnerPrimes line 15
  2. theorem OAI.Erdos970.NumberTheoryLean.WrongOwnerBinMass.wrongOwnerPrimes_none line 19
  3. theorem OAI.Erdos970.NumberTheoryLean.WrongOwnerBinMass.wrongOwnerPrimes_self line 24
  4. theorem OAI.Erdos970.NumberTheoryLean.WrongOwnerBinMass.wrongOwnerPrimes_eq_common line 29
  5. theorem OAI.Erdos970.NumberTheoryLean.WrongOwnerBinMass.wrong_owner_mass_bound line 35
  6. theorem OAI.Erdos970.NumberTheoryLean.WrongOwnerFraction.uniform_bin_mass_lower line 82
  7. theorem OAI.Erdos970.NumberTheoryLean.WrongOwnerFraction.uniform_wrong_owner_fraction line 105
  8. theorem OAI.Erdos970.NumberTheoryLean.WrongOwnerSearchTail.search_fraction_factor line 134
  9. theorem OAI.Erdos970.NumberTheoryLean.WrongOwnerSearchTail.actual_wrong_search_mass line 158
  10. theorem OAI.Erdos970.NumberTheoryLean.WrongOwnerBoxMass.wrong_owner_box_mass line 185
  11. theorem OAI.Erdos970.NumberTheoryLean.WrongOwnerBoxMass.logarithmic_positions_le_w line 200
  12. theorem OAI.Erdos970.NumberTheoryLean.WrongOwnerBoxMass.length_bounded_wrong_box_mass line 214