OAI/Probability/SignedSweeps/CoefficientUniform.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.coefficientPush_comp line 11
2. lemma OAI.SignedSweeps.coefficientPush_equiv line 18
3. def OAI.SignedSweeps.subgroupAverageCoefficient line 24
4. lemma OAI.SignedSweeps.subgroupAverageCoefficient_equiv line 27
5. lemma OAI.SignedSweeps.subgroupAverageCoefficient_image line 36
6. lemma OAI.SignedSweeps.coefficientAction_subgroupAverage line 58
7. lemma OAI.SignedSweeps.subgroupAverageCoefficient_support line 66
8. def OAI.SignedSweeps.piHom line 79
9. lemma OAI.SignedSweeps.piHom_injective line 85
10. lemma OAI.SignedSweeps.productCoefficient_push line 93
11. lemma OAI.SignedSweeps.product_subgroupAverage line 114