OAI/Probability/SKBarriers/Scalar/ScalarPositiveHessian.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.scalarPath_terminal_affine_shift line 14
2. theorem OAI.SK.Analytic.scalarPath_square_bound_shift line 24
3. theorem OAI.SK.Analytic.scalarHierarchyAverage_square_gap_compact line 38