OAI/Combinatorics/Progressions/Lattices/IntegerImageProbabilityLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.normalizedIntegerFiberOutputMass line 13
2. def OAI.Erdos3.normalizedFiberErrorConstant line 18
3. theorem OAI.Erdos3.normalizedIntegerFiberOutputMass_pmf line 22
4. theorem OAI.Erdos3.normalizedIntegerFiber_uniform_error line 31
5. theorem OAI.Erdos3.integerImagePMF_measure_map line 82
6. theorem OAI.Erdos3.integerImagePMF_singleton line 92
7. theorem OAI.Erdos3.integerImagePMF_zero_off_image line 102
8. theorem OAI.Erdos3.normalizedIntegerFiberOutputMass_zero_off_image line 113