OAI/Combinatorics/SharpThreshold/MeanEndpoints.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem313.continuous_graphWeight line 9
2. lemma OAI.Problem313.continuous_graphMean line 17
3. lemma OAI.Problem313.increasing_nontrivial_false line 25
4. lemma OAI.Problem313.increasing_nontrivial_true line 35
5. lemma OAI.Problem313.graphWeight_zero line 41
6. lemma OAI.Problem313.graphWeight_one line 59
7. lemma OAI.Problem313.graphMean_zero_eq line 77
8. lemma OAI.Problem313.graphMean_one_eq line 82
9. lemma OAI.Problem313.graphMean_zero_of_increasing_nontrivial line 87
10. lemma OAI.Problem313.graphMean_one_of_increasing_nontrivial line 93