OAI/NumberTheory/Catalan/Arithmetic/FixedAuxiliaryIntegerPilot.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedClearedMoment47 line 11
  2. theorem OAI.InternalCatalan.fixedFilteredMoment47_cleared line 62
  3. def OAI.InternalCatalan.fixedClearedZeta47 line 70
  4. theorem OAI.InternalCatalan.fixedFilteredZeta47_cleared line 120
  5. theorem OAI.InternalCatalan.fixedIntegerFractionSum line 128
  6. theorem OAI.InternalCatalan.fixedIntegerSumLink line 137
  7. theorem OAI.InternalCatalan.fixedAuxiliaryPartialP_0 line 143
  8. theorem OAI.InternalCatalan.fixedAuxiliaryChunkP_0 line 145
  9. theorem OAI.InternalCatalan.fixedAuxiliaryPartialP_8 line 149
  10. theorem OAI.InternalCatalan.fixedAuxiliaryChunkP_8 line 157
  11. theorem OAI.InternalCatalan.fixedAuxiliaryPartialP_16 line 161
  12. theorem OAI.InternalCatalan.fixedAuxiliaryChunkP_16 line 169
  13. theorem OAI.InternalCatalan.fixedAuxiliaryPartialP_24 line 173
  14. theorem OAI.InternalCatalan.fixedAuxiliaryChunkP_24 line 181
  15. theorem OAI.InternalCatalan.fixedAuxiliaryPartialP_32 line 185
  16. theorem OAI.InternalCatalan.fixedAuxiliaryChunkP_32 line 193
  17. theorem OAI.InternalCatalan.fixedAuxiliaryPartialP_40 line 197
  18. theorem OAI.InternalCatalan.fixedAuxiliaryChunkP_40 line 205
  19. theorem OAI.InternalCatalan.fixedAuxiliaryPartialP_48 line 209
  20. theorem OAI.InternalCatalan.fixedAuxiliaryChunkP_48 line 217
  21. theorem OAI.InternalCatalan.fixedAuxiliaryPartialP_56 line 221
  22. theorem OAI.InternalCatalan.fixedAuxiliaryChunkP_56 line 229
  23. theorem OAI.InternalCatalan.fixedAuxiliaryPartialP_64 line 233
  24. theorem OAI.InternalCatalan.fixedAuxiliaryChunkP_64 line 241
  25. theorem OAI.InternalCatalan.fixedAuxiliaryPartialP_65 line 245
  26. theorem OAI.InternalCatalan.fixedAuxiliaryIntegerDotP line 253
  27. theorem OAI.InternalCatalan.fixedAuxiliaryFractionDotP line 257
  28. theorem OAI.InternalCatalan.fixedAuxiliaryPartialD_0 line 273
  29. theorem OAI.InternalCatalan.fixedAuxiliaryChunkD_0 line 275
  30. theorem OAI.InternalCatalan.fixedAuxiliaryPartialD_8 line 279
  31. theorem OAI.InternalCatalan.fixedAuxiliaryChunkD_8 line 287
  32. theorem OAI.InternalCatalan.fixedAuxiliaryPartialD_16 line 291
  33. theorem OAI.InternalCatalan.fixedAuxiliaryChunkD_16 line 299
  34. theorem OAI.InternalCatalan.fixedAuxiliaryPartialD_24 line 303
  35. theorem OAI.InternalCatalan.fixedAuxiliaryChunkD_24 line 311
  36. theorem OAI.InternalCatalan.fixedAuxiliaryPartialD_32 line 315
  37. theorem OAI.InternalCatalan.fixedAuxiliaryChunkD_32 line 323
  38. theorem OAI.InternalCatalan.fixedAuxiliaryPartialD_40 line 327
  39. theorem OAI.InternalCatalan.fixedAuxiliaryChunkD_40 line 335
  40. theorem OAI.InternalCatalan.fixedAuxiliaryPartialD_48 line 339
  41. theorem OAI.InternalCatalan.fixedAuxiliaryChunkD_48 line 347
  42. theorem OAI.InternalCatalan.fixedAuxiliaryPartialD_56 line 351
  43. theorem OAI.InternalCatalan.fixedAuxiliaryChunkD_56 line 359
  44. theorem OAI.InternalCatalan.fixedAuxiliaryPartialD_64 line 363
  45. theorem OAI.InternalCatalan.fixedAuxiliaryChunkD_64 line 371
  46. theorem OAI.InternalCatalan.fixedAuxiliaryPartialD_65 line 375
  47. theorem OAI.InternalCatalan.fixedAuxiliaryIntegerDotD line 383
  48. theorem OAI.InternalCatalan.fixedAuxiliaryFractionDotD line 387
  49. theorem OAI.InternalCatalan.fixedBaseEntry_48_47_integer line 403
  50. theorem OAI.InternalCatalan.fixedBaseEntry_48_47_scaled_integer line 413