OAI/NumberTheory/Ostmann/Arithmetic/PrimeSquareLiftFamilies.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.affineSwapEquiv line 9
  2. def OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.affineRowEquiv line 17
  3. def OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.row line 27
  4. theorem OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.row_card line 30
  5. theorem OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.row_probability line 37
  6. def OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.badLifts line 46
  7. def OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.survivingLifts line 50
  8. theorem OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.mem_badLifts line 52
  9. theorem OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.mem_survivingLifts line 57
  10. theorem OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.badLifts_card_le line 62
  11. theorem OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.badLifts_probability_le line 70
  12. theorem OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.survivingLifts_probability_ge line 83
  13. theorem OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.bounded_test_loss line 96
  14. theorem OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.square_divides_some_lift_iff line 123
  15. def OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.integerBadLifts line 135
  16. theorem OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.integerBadLifts_eq line 140
  17. theorem OAI.Ostmann.Arithmetic.PrimeSquareLiftFamilies.integer_bad_lift_probability_le line 151