OAI/NumberTheory/Jacobsthal/Estimates/AdmittedHighRemoval.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.AdmittedHighRemoval.pow_map_state line 17
  2. theorem OAI.Erdos970.NumberTheoryLean.AdmittedHighRemoval.pow_map_coordinates_le line 22
  3. def OAI.Erdos970.NumberTheoryLean.AdmittedHighRemoval.lowHighMass line 28
  4. def OAI.Erdos970.NumberTheoryLean.AdmittedHighRemoval.reward line 32
  5. def OAI.Erdos970.NumberTheoryLean.AdmittedHighRemoval.rewardedHighMass line 35
  6. theorem OAI.Erdos970.NumberTheoryLean.AdmittedHighRemoval.low_mass_le_unrestricted line 38
  7. theorem OAI.Erdos970.NumberTheoryLean.AdmittedHighRemoval.reward_mass_le_unrestricted line 52
  8. theorem OAI.Erdos970.NumberTheoryLean.AdmittedHighRemoval.low_gap_high_removal line 62
  9. theorem OAI.Erdos970.NumberTheoryLean.AdmittedHighRemoval.rewarded_high_removal line 72