OAI/Probability/BinarySweep/SparseBounds/CenteredMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Irrep.groupAverage_adjoint line 14
2. lemma OAI.BinaryCoordinateSweeps.Irrep.even_compatible_maps line 21
3. theorem OAI.BinaryCoordinateSweeps.Irrep.evenMoment_le_of_injective line 32
4. theorem OAI.BinaryCoordinateSweeps.Young.centeredHilbert_moment line 62