OAI/Combinatorics/SumProduct/Alignment/CorrectedBox04.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CorrectedBoxLeibman.direction_character_recovery line 28
2. def OAI.CorrectedBoxLeibman.gridExponent line 113
3. lemma OAI.CorrectedBoxLeibman.gridExponent_apply line 115
4. lemma OAI.CorrectedBoxLeibman.gridExponent_injective line 116
5. lemma OAI.CorrectedBoxLeibman.gridExponent_degree line 121
6. lemma OAI.CorrectedBoxLeibman.gridMonomial_eq_prod line 126
7. lemma OAI.CorrectedBoxLeibman.rescale_line_bound line 141
8. theorem OAI.CorrectedBoxLeibman.corrected_box_recovery line 159
9. lemma OAI.CorrectedBoxLeibman.character_pow_toAdd line 239
10. lemma OAI.CorrectedBoxLeibman.character_pow_ne line 244
11. theorem OAI.CorrectedBoxLeibman.box_monomial_large line 258