OAI/Probability/SKBarriers/Hierarchy/HierarchyMomentLevels.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.TranslationInvariant.directionalGradient line 31
2. theorem OAI.SK.Analytic.gaussianAverage_const_prefix line 39
3. theorem OAI.SK.Analytic.TranslationInvariant.gaussianAverage line 45
4. def OAI.SK.Analytic.hierarchyMomentLevel line 57
5. theorem OAI.SK.Analytic.hierarchyMomentLevel_bounded_continuous line 64
6. theorem OAI.SK.Analytic.hierarchyMomentLevel_invariant_of_tail line 81
7. theorem OAI.SK.Analytic.hierarchyAverage_momentLevel line 100
8. theorem OAI.SK.Analytic.hierarchyLevel_gradient line 112