OAI/Combinatorics/Progressions/Sampling/JointGridAccuracy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Erdos3.oddTorusFactor_neZero line 12
2. theorem OAI.Erdos3.jointImageMass_eq_grid_product line 14
3. theorem OAI.Erdos3.jointImageMass_at_representatives line 30
4. theorem OAI.Erdos3.jointGridDensity_total line 44
5. def OAI.Erdos3.jointGridAxisTolerance line 69
6. theorem OAI.Erdos3.jointGridAxisTolerance_spec line 71
7. theorem OAI.Erdos3.joint_integer_density_approximation line 83