OAI/Combinatorics/SquareDifference/BlockAverage.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SquareDifference.cyclic_ascent_of_start_ne line 15
2. lemma OAI.SquareDifference.tuple_interval_ascent line 30
3. lemma OAI.SquareDifference.cycleVertex_consecutive_ne line 36
4. lemma OAI.SquareDifference.equal_choice_probability line 42
5. lemma OAI.SquareDifference.choice_average_bound line 51
6. lemma OAI.SquareDifference.multilinearIntegral_scale_expect line 68