OAI/Combinatorics/Progressions/Estimates/FiniteGoodPartTransfer.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_weight_pos line 13
2. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_weight_ne_zero line 20
3. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_goodPart_comparison line 34
4. def OAI.Erdos3.FiniteProbabilityWeights.goodPartBaseMean line 54
5. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_goodPart_base_comparison line 59
6. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_div line 87
7. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_positive_weight_ge_mean line 91
8. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_positive_weight_ge_complexMean_re line 110
9. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_good_base_of_le_re line 115
10. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_normalized_good_cell_of_le_re line 133
11. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_good_base_of_comparison line 159
12. theorem OAI.Erdos3.FiniteProbabilityWeights.goodPartBaseMean_sub_norm_le line 183
13. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_goodPart_base_transfer line 201