OAI/NumberTheory/Catalan/Arithmetic/OddPrimeLoss.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.oddPrimeLoss line 16
  2. theorem OAI.InternalCatalan.continuous_oddPrimeLoss line 21
  3. theorem OAI.InternalCatalan.oddPrimeLoss_of_le_25 line 25
  4. theorem OAI.InternalCatalan.oddPrimeLoss_25_29 line 38
  5. theorem OAI.InternalCatalan.oddPrimeLoss_29_65div2 line 51
  6. theorem OAI.InternalCatalan.oddPrimeLoss_65div2_69div2 line 64
  7. theorem OAI.InternalCatalan.oddPrimeLoss_69div2_40 line 77
  8. theorem OAI.InternalCatalan.oddPrimeLoss_40_58 line 90
  9. theorem OAI.InternalCatalan.oddPrimeLoss_58_59 line 103
  10. theorem OAI.InternalCatalan.oddPrimeLoss_59_65 line 116
  11. theorem OAI.InternalCatalan.oddPrimeLoss_of_ge_65 line 129
  12. theorem OAI.InternalCatalan.oddPrimeLoss_mem_Icc line 142
  13. theorem OAI.InternalCatalan.oddPrimeLoss_nonneg line 170
  14. theorem OAI.InternalCatalan.oddPrimeLoss_le line 173
  15. theorem OAI.InternalCatalan.loss_integral_affine line 176
  16. theorem OAI.InternalCatalan.integral_oddPrimeLoss_0_25 line 186
  17. theorem OAI.InternalCatalan.integral_oddPrimeLoss_25_29 line 197
  18. theorem OAI.InternalCatalan.integral_oddPrimeLoss_29_65div2 line 208
  19. theorem OAI.InternalCatalan.integral_oddPrimeLoss_65div2_69div2 line 219
  20. theorem OAI.InternalCatalan.integral_oddPrimeLoss_69div2_40 line 230
  21. theorem OAI.InternalCatalan.integral_oddPrimeLoss_40_58 line 241
  22. theorem OAI.InternalCatalan.integral_oddPrimeLoss_58_59 line 252
  23. theorem OAI.InternalCatalan.integral_oddPrimeLoss_59_65 line 263
  24. theorem OAI.InternalCatalan.integral_oddPrimeLoss line 277
  25. theorem OAI.InternalCatalan.integral_oddPrimeLoss_25_65 line 310