OAI/Combinatorics/Progressions/Probability/DensityNormalizationScales.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.log_two_add_le_of_le_exp line 10
2. theorem OAI.Erdos3.baseline_scale_inv_le line 21
3. theorem OAI.Erdos3.weighted_scale_inv_le line 25
4. theorem OAI.Erdos3.site_normalization_caps line 31