OAI/Combinatorics/Progressions/Sampling/ShiftedSmoothFiniteGridLaw.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.shiftedSmoothProductPMF_positive_coord_lt line 10
  2. def OAI.Erdos3.shiftedSmoothPositiveGrid line 25
  3. theorem OAI.Erdos3.shiftedSmoothPositiveGrid_zero_off line 31
  4. theorem OAI.Erdos3.shiftedSmoothPositiveGrid_coord_lt line 41
  5. def OAI.Erdos3.shiftedSmoothPositiveGridWeights line 47
  6. theorem OAI.Erdos3.shiftedSmoothPositiveGridWeights_weight line 53
  7. theorem OAI.Erdos3.shiftedSmoothPositiveGridWeights_weight_pos line 59
  8. theorem OAI.Erdos3.shiftedSmoothPositiveGridWeights_event_eq_map_true line 65
  9. theorem OAI.Erdos3.rectangularWeightIndices_normalized_bound line 86
  10. theorem OAI.Erdos3.rectangularLatticePoint_injective line 96
  11. theorem OAI.Erdos3.shiftedSmoothProductPMF_point_le line 107
  12. theorem OAI.Erdos3.shiftedSmoothProductFiniteWeights_point_le line 120
  13. theorem OAI.Erdos3.shiftedSmoothProductFiniteWeights_mean_eq_tsum line 128
  14. theorem OAI.Erdos3.shiftedSmoothProductFiniteWeights_event_eq_map line 140
  15. theorem OAI.Erdos3.shiftedSmoothPositiveGridWeights_point_le line 152
  16. theorem OAI.Erdos3.shiftedSmoothScale_mesh_le_quarter line 160