OAI/Combinatorics/Progressions/Lattices/IntegerRowInterpolationMixture.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.affineProfile_sample_coordinate line 14
  2. theorem OAI.Erdos3.affineProductProfile_sample line 18
  3. theorem OAI.Erdos3.affineProductProfile_sample_sum line 28
  4. theorem OAI.Erdos3.affineProfile_coordinate_sum_pos line 36
  5. theorem OAI.Erdos3.affineProductProfile_sample_sum_pos line 50
  6. theorem OAI.Erdos3.affineCoefficientPMF_apply line 58
  7. def OAI.Erdos3.normalizedIntegerPMF line 81
  8. theorem OAI.Erdos3.normalizedIntegerPMF_apply line 86
  9. theorem OAI.Erdos3.normalizedIntegerPMF_support line 93
  10. theorem OAI.Erdos3.normalizedIntegerPMF_cap line 104
  11. def OAI.Erdos3.normalizedIntegerInterpolation line 112
  12. theorem OAI.Erdos3.normalizedIntegerInterpolation_grid line 115
  13. theorem OAI.Erdos3.normalizedIntegerInterpolation_contDiff line 122
  14. theorem OAI.Erdos3.normalizedIntegerInterpolation_range line 128
  15. theorem OAI.Erdos3.normalizedIntegerInterpolation_zero line 143
  16. def OAI.Erdos3.constantIntegerPMF line 160
  17. theorem OAI.Erdos3.constantIntegerPMF_large line 165
  18. theorem OAI.Erdos3.constantIntegerPMF_small line 170
  19. theorem OAI.Erdos3.constantIntegerPMF_support line 178
  20. theorem OAI.Erdos3.constantIntegerPMF_cap line 190
  21. def OAI.Erdos3.IsIntegerMassInterpolation line 213
  22. theorem OAI.Erdos3.IsIntegerMassInterpolation.lipschitz line 218
  23. theorem OAI.Erdos3.IsIntegerMassInterpolation.mono line 225
  24. theorem OAI.Erdos3.normalizedIntegerInterpolation_difference line 231
  25. theorem OAI.Erdos3.normalizedIntegerInterpolation_spec line 255
  26. theorem OAI.Erdos3.normalizedIntegerInterpolation_lipschitz_bound line 273
  27. theorem OAI.Erdos3.normalizedIntegerInterpolation_lipschitz line 298
  28. def OAI.Erdos3.integerMassTent line 316
  29. theorem OAI.Erdos3.integerMassTent_grid line 319
  30. theorem OAI.Erdos3.integerMassTent_range line 332
  31. theorem OAI.Erdos3.integerMassTent_difference line 339
  32. theorem OAI.Erdos3.integerMassTent_spec line 357
  33. theorem OAI.Erdos3.affineCoefficientImage_enormous_error line 371
  34. def OAI.Erdos3.constantIntegerInterpolation line 406
  35. def OAI.Erdos3.constantIntegerInterpolationCap line 410
  36. def OAI.Erdos3.constantIntegerInterpolationLip line 413
  37. theorem OAI.Erdos3.constantIntegerInterpolation_spec line 417
  38. def OAI.Erdos3.integerPointDensity line 444
  39. theorem OAI.Erdos3.integerPointDensity_grid line 447
  40. theorem OAI.Erdos3.integerPointDensity_range line 460
  41. theorem OAI.Erdos3.integerPointDensity_difference line 467
  42. theorem OAI.Erdos3.integerPointDensity_lipschitz line 480
  43. theorem OAI.Erdos3.integerPointDensity_support line 486
  44. theorem OAI.Erdos3.integerPointDensity_support_quarter line 492
  45. theorem OAI.Erdos3.integerPointDensity_spec line 501
  46. def OAI.Erdos3.integerRowMassTent line 519
  47. theorem OAI.Erdos3.integerRowMassTent_range line 522
  48. theorem OAI.Erdos3.integerRowMassTent_grid line 530
  49. theorem OAI.Erdos3.integerRowMassTent_lipschitz line 544
  50. def OAI.Erdos3.integerRowMassInterpolation line 559
  51. theorem OAI.Erdos3.integerRowMassTent_integrable line 562
  52. theorem OAI.Erdos3.integerRowMassInterpolation_range line 569
  53. theorem OAI.Erdos3.integerRowMassInterpolation_grid line 577
  54. theorem OAI.Erdos3.integerRowMassInterpolation_lipschitz line 588
  55. def OAI.Erdos3.normalizedIntegerRowInterpolation line 615
  56. theorem OAI.Erdos3.normalizedIntegerRowInterpolation_range line 618
  57. theorem OAI.Erdos3.normalizedIntegerRowInterpolation_grid line 624
  58. theorem OAI.Erdos3.normalizedIntegerRowInterpolation_lipschitz line 630
  59. theorem OAI.Erdos3.integerRowMassInterpolation_bind line 659
  60. theorem OAI.Erdos3.normalizedIntegerRowInterpolation_bind line 673
  61. theorem OAI.Erdos3.integerRowMassInterpolation_finite_bind line 681
  62. theorem OAI.Erdos3.normalizedIntegerRowInterpolation_finite_bind line 689