OAI/Combinatorics/Progressions/Sampling/RelativePatchScoreObstruction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.relativePatchBoxScore_nonpos_of_one_le line 10
2. theorem OAI.Erdos3.relativePatchSliceScore_nonpos_of_one_le line 23
3. theorem OAI.Erdos3.RelativePatchSliceConclusion.target_lt_one line 39
4. theorem OAI.Erdos3.RelativePatchAbsoluteRule.mean_lt_of_one_le_target line 49