OAI/Probability/SKBarriers/Hierarchy/TimeChainOnAnalytic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.TimeChainOn.sub_nonneg line 16
2. theorem OAI.SK.Analytic.TimeChainOn.nn_duration line 19
3. theorem OAI.SK.Analytic.TimeChainOn.nn_le_one line 24
4. theorem OAI.SK.Analytic.TimeChainOn.scalar_operator line 28
5. theorem OAI.SK.Analytic.TimeChainOn.scalar_value line 37
6. theorem OAI.SK.Analytic.TimeChainOn.scalar_hessian line 44
7. theorem OAI.SK.Analytic.TimeChainOn.scalar_average line 51
8. theorem OAI.SK.Analytic.TimeChainOn.scalar_susceptibility line 62
9. theorem OAI.SK.Analytic.TimeChainOn.area line 78
10. theorem OAI.SK.Analytic.TimeChainOn.penalty line 82