OAI/Probability/ClassicalON/ModeCosts.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClassicalON.LatticeGraph.mode_gradient_square_sum_le line 11
2. theorem OAI.ClassicalON.LatticeGraph.mode_sup_square_le line 21
3. theorem OAI.ClassicalON.LatticeGraph.mode_gram_reweight line 30
4. theorem OAI.ClassicalON.LatticeGraph.mode_group_gram_bound line 46
5. abbrev OAI.ClassicalON.LatticeGraph.ModeIndex line 58
6. def OAI.ClassicalON.LatticeGraph.modes line 60
7. def OAI.ClassicalON.LatticeGraph.modeDifferences line 63
8. theorem OAI.ClassicalON.LatticeGraph.modes_HS_bound line 66
9. theorem OAI.ClassicalON.LatticeGraph.modes_min_bound line 78