OAI/Combinatorics/Progressions/Lattices/UniformResidueSmallPeriod.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.uniformPMF_map_fiber line 11
  2. theorem OAI.Erdos3.uniformPMF_map_hom_image line 22
  3. theorem OAI.Erdos3.uniformPMF_map_hom_index line 46
  4. theorem OAI.Erdos3.uniformResidueMatrix_image_mask line 64
  5. theorem OAI.Erdos3.residueLatticeImage_index_le_period line 91
  6. theorem OAI.Erdos3.uniformResidueMatrix_density_bound line 105
  7. theorem OAI.Erdos3.uniformResidueMatrix_family_density_bound line 131
  8. theorem OAI.Erdos3.uniformPMF_map_hom_toReal_eq_of_sub_mem line 158
  9. theorem OAI.Erdos3.uniformResidueMatrix_toReal_eq_of_period line 171
  10. def OAI.Erdos3.uniformResidueSmallPeriodDensity line 189
  11. theorem OAI.Erdos3.uniformResidueSmallPeriodDensity_apply line 197
  12. theorem OAI.Erdos3.uniformResidueSmallPeriodDensity_bounds line 213