OAI/NumberTheory/Ostmann/Tree/CycleProjection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.Tree.average_fintype_congr line 11
2. lemma OAI.Ostmann.Tree.real_average_fintype_congr line 15
3. lemma OAI.Ostmann.Tree.average_mul_const line 20
4. lemma OAI.Ostmann.Tree.average_const line 24
5. lemma OAI.Ostmann.Tree.average_comm line 29
6. def OAI.Ostmann.Tree.BalancedSelection.projection line 35
7. theorem OAI.Ostmann.Tree.cycle_projection_correlation line 40
8. theorem OAI.Ostmann.Tree.cycle_projection_reduction line 68