OAI/Combinatorics/SumProduct/Alignment/SquareInduction02.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SquareInduction.compact_horizontal_representatives line 29
2. lemma OAI.SquareInduction.square_shift_scales line 51
3. theorem OAI.SquareInduction.quadratic_vertical_correlation line 100
4. lemma OAI.SquareInduction.integer_linear_return line 165
5. theorem OAI.SquareInduction.quadratic_vertical_correlation_unbounded_linear line 205
6. theorem OAI.SquareInduction.quadratic_source_vertical_correlation line 256