OAI/Combinatorics/Progressions/Lattices/SelectedResidueApproximation.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerRowShift line 15
  2. theorem OAI.Erdos3.integerRowShift_real line 19
  3. theorem OAI.Erdos3.integerRowShift_bound line 27
  4. theorem OAI.Erdos3.integerRowShift_normalized_bound line 46
  5. def OAI.Erdos3.residueLatticeArray line 69
  6. def OAI.Erdos3.residueProfileCenter line 73
  7. def OAI.Erdos3.residueProfileWidth line 77
  8. theorem OAI.Erdos3.residueProfileWidth_pos line 80
  9. theorem OAI.Erdos3.residueLatticeArray_rowShift line 85
  10. theorem OAI.Erdos3.residueRowShift_normalized_bound line 101
  11. theorem OAI.Erdos3.residueProfile_point line 130
  12. def OAI.Erdos3.residueSmoothIndexPMF line 142
  13. theorem OAI.Erdos3.residueSmoothIndexPMF_toReal line 150
  14. theorem OAI.Erdos3.residueLatticeArray_injective line 170
  15. theorem OAI.Erdos3.residueLatticeArray_range line 178
  16. def OAI.Erdos3.residueSmoothPMF line 193
  17. theorem OAI.Erdos3.residueSmoothPMF_at line 201
  18. theorem OAI.Erdos3.residueSmoothPMF_zero_off line 214
  19. theorem OAI.Erdos3.residueSmoothPMF_expectation line 223
  20. def OAI.Erdos3.residueSmoothScalarPMFs line 241
  21. theorem OAI.Erdos3.residueSmoothIndexPMF_eq_independent line 253
  22. theorem OAI.Erdos3.residueSmoothIndexPMF_selected_marginal line 264
  23. theorem OAI.Erdos3.residue_smooth_row_shift_transfer line 287
  24. theorem OAI.Erdos3.residue_smooth_row_shift_transfer_lipschitz_amplitude line 330
  25. def OAI.Erdos3.residueSmoothWeight line 377
  26. theorem OAI.Erdos3.residueSmoothWeight_at line 383
  27. theorem OAI.Erdos3.residueSmoothWeight_mass line 390
  28. theorem OAI.Erdos3.residueSmoothPMF_conditional_weight line 405
  29. theorem OAI.Erdos3.rowShiftedTuple_add_base line 432
  30. theorem OAI.Erdos3.anchored_residue_smooth_row_shift_transfer line 440
  31. abbrev OAI.Erdos3.ColumnResiduePattern line 477
  32. def OAI.Erdos3.columnResiduePattern line 480
  33. def OAI.Erdos3.columnResidueRepresentative line 483
  34. theorem OAI.Erdos3.columnResidueRepresentative_cast line 487
  35. theorem OAI.Erdos3.columnResiduePattern_eq_iff line 492
  36. theorem OAI.Erdos3.residueSmoothWeight_eq_pattern line 507
  37. theorem OAI.Erdos3.integerArrayFrame_add line 524
  38. theorem OAI.Erdos3.residueSmoothWeight_congr line 538
  39. theorem OAI.Erdos3.residueSmoothMass_congr line 556
  40. theorem OAI.Erdos3.residueSmoothPMF_congr line 565
  41. def OAI.Erdos3.boundedColumnResidueRepresentative line 576
  42. theorem OAI.Erdos3.boundedColumnResidueRepresentative_congr line 580
  43. theorem OAI.Erdos3.boundedColumnResidueRepresentative_bounds line 588
  44. theorem OAI.Erdos3.residueSmoothPMF_bounded line 595
  45. def OAI.Erdos3.selectedResidueSmoothWeight line 618
  46. theorem OAI.Erdos3.selectedResidueSmoothWeight_eq_sum line 624
  47. theorem OAI.Erdos3.residueSmoothWeight_zero_off line 636
  48. theorem OAI.Erdos3.selectedResidueSmoothWeight_nonneg line 645
  49. theorem OAI.Erdos3.selectedResidueSmoothWeight_zero_off line 653
  50. theorem OAI.Erdos3.selectedResidueSmoothWeight_mass line 661
  51. theorem OAI.Erdos3.selectedResidueSmoothWeight_summable line 680
  52. theorem OAI.Erdos3.selectedResidueSmoothWeight_mass_pos line 685
  53. def OAI.Erdos3.selectedResidueSmoothPMF line 695
  54. theorem OAI.Erdos3.selectedResidueSmoothPMF_toReal line 703
  55. theorem OAI.Erdos3.selectedResidueSmoothPMF_mixture line 711
  56. theorem OAI.Erdos3.selectedResidueSmoothPMF_bound_of_cells line 733
  57. theorem OAI.Erdos3.selectedResidueSmoothPMF_approximation line 766
  58. theorem OAI.Erdos3.selectedResidueSmoothPMF_projection_approximation line 780