OAI/Combinatorics/Progressions/Estimates/AdaptiveRatioNormalization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.abs_mul_sub_one_of_near_one line 9
2. theorem OAI.Erdos3.FiniteProbabilityWeights.abs_mean_product_sub_one line 25
3. theorem OAI.Erdos3.adaptive_ratio_product_close line 48
4. theorem OAI.Erdos3.adaptive_ratio_product_le line 59
5. theorem OAI.Erdos3.productTruncatedPairing_leaf_normalized_bound line 70