OAI/Probability/BinarySweep/SparseBounds/ManySparse.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinaryCoordinateSweeps.conditional_specht_many_sparse_eventually line 18
2. lemma OAI.BinaryCoordinateSweeps.Irrep.sum_pow_le_sum_pow line 52
3. lemma OAI.BinaryCoordinateSweeps.Irrep.evenMoment_le_one_pow line 67
4. lemma OAI.BinaryCoordinateSweeps.Irrep.evenMoment_le_exp line 79
5. def OAI.BinaryCoordinateSweeps.mainMomentPower line 95
6. theorem OAI.BinaryCoordinateSweeps.sparse_uniform_radius line 97
7. theorem OAI.BinaryCoordinateSweeps.sparse_closing_radius line 172