OAI/Probability/SKBarriers/Hierarchy/CascadeRecursion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.CascadeSpace line 25
2. instance OAI.SK.Analytic.cascadeNormedGroup line 29
3. instance OAI.SK.Analytic.cascadeNormedSpace line 35
4. def OAI.SK.Analytic.cascadeLift line 44
5. def OAI.SK.Analytic.cascadePressure line 48
6. def OAI.SK.Analytic.cascadeMoment line 52
7. theorem OAI.SK.Analytic.cascadePressure_boundedDerivs line 58
8. theorem OAI.SK.Analytic.cascadeMoment_bounded_continuous line 64
9. theorem OAI.SK.Analytic.cascadePressure_gradient line 74
10. theorem OAI.SK.Analytic.cascade_curvature_domination line 85