OAI/Probability/SignedSweeps/GroupAverage.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedSweeps.groupAverage line 10
2. lemma OAI.SignedSweeps.groupAverage_invariant line 14
3. lemma OAI.SignedSweeps.groupAverage_fixed line 23
4. lemma OAI.SignedSweeps.groupAverage_idempotent line 31
5. lemma OAI.SignedSweeps.representation_inner_inverse line 37
6. lemma OAI.SignedSweeps.groupAverage_symmetric line 48
7. lemma OAI.SignedSweeps.symmetricProjection_norm_eq_iff line 58
8. lemma OAI.SignedSweeps.groupAverage_norm_eq_iff line 74
9. lemma OAI.SignedSweeps.layerOperator_symmetricProjection line 84
10. lemma OAI.SignedSweeps.layerOperator_norm_eq_iff line 91
11. lemma OAI.SignedSweeps.list_prod_norm_eq_fixed line 98
12. lemma OAI.SignedSweeps.sweep_norm_eq_implies_layer_fixed line 119
13. lemma OAI.SignedSweeps.opNorm_lt_one_of_pointwise line 134