OAI/Combinatorics/Progressions/Linear/FiniteMarginalProjection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.finiteWeightDensity_mean_le line 13
2. theorem OAI.Erdos3.zeroLevelGram_bound line 25
3. theorem OAI.Erdos3.finiteLaw_zero_projection line 41
4. theorem OAI.Erdos3.approxProduct_projection_bound line 92
5. theorem OAI.Erdos3.finiteLaw_projection_positive line 119
6. theorem OAI.Erdos3.finiteLaw_projection_bound line 150
7. theorem OAI.Erdos3.finiteLaw_projection_of_density line 165
8. theorem OAI.Erdos3.marginal_mass_error_of_density line 199
9. theorem OAI.Erdos3.finiteProbability_truncated_projection line 214