OAI/Probability/SKBarriers/Hierarchy/HierarchyProbability.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.hierarchyMomentLevel_nonneg line 15
2. theorem OAI.SK.Analytic.hierarchyMomentLevel_const line 28
3. theorem OAI.SK.Analytic.hierarchyMomentLevel_const_mul line 39
4. theorem OAI.SK.Analytic.hierarchyMomentLevel_sum line 52
5. theorem OAI.SK.Analytic.hierarchySpinWeight_regular line 79
6. theorem OAI.SK.Analytic.hierarchySpinWeight_nonneg line 86
7. theorem OAI.SK.Analytic.hierarchySpinWeight_sum line 90
8. theorem OAI.SK.Analytic.hierarchySpinMean_eq_sum line 101