OAI/Probability/SKBarriers/Scalar/TiltedTerminalLimit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.hierarchyPressure_rootGradient_lipschitz line 17
2. theorem OAI.SK.Analytic.scalarHierarchy_primitive_regular line 35
3. theorem OAI.SK.Analytic.scalarHierarchy_primitive_derivative_lipschitz line 42
4. theorem OAI.SK.Analytic.dyadicScalar_primitive_regular line 59
5. theorem OAI.SK.Analytic.dyadicScalar_primitive_derivative_lipschitz line 65
6. def OAI.SK.Analytic.scalarCDFTerminalDerivative line 77
7. theorem OAI.SK.Analytic.dyadicScalar_primitive_uniform line 81
8. theorem OAI.SK.Analytic.dyadicScalar_terminal_derivative_uniform line 93
9. theorem OAI.SK.Analytic.scalarCDFOperator_terminal_hasDerivAt line 108