OAI/Combinatorics/Progressions/Geometry/FiniteGoodSupport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_congr_on_support line 12
2. theorem OAI.Erdos3.restrictedChartDensity_eq_of_values line 29
3. theorem OAI.Erdos3.restrictedChartDensity_pointwise_comparison line 38
4. theorem OAI.Erdos3.restrictedChartDensity_bound line 49
5. theorem OAI.Erdos3.restrictedChartDensity_mean_comparison line 57
6. theorem OAI.Erdos3.restrictedChartDensity_sub line 79
7. theorem OAI.Erdos3.restrictedChartDensity_abs line 88
8. theorem OAI.Erdos3.restrictedChartDensity_abs_sub line 97
9. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_supported_good_of_bad_lt_one line 113
10. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_goodPart_exp_error line 125