OAI/Probability/SKBarriers/Replicas/TripleCDFTrial.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.tripleTimeCommonError line 16
2. def OAI.SK.Analytic.tripleCDFResponse line 20
3. def OAI.SK.Analytic.tripleCDFTrialCoefficient line 24
4. theorem OAI.SK.Analytic.crossPenalty_response_le line 29
5. theorem OAI.SK.Analytic.TripleTimeBlocks.common_error line 42
6. theorem OAI.SK.Analytic.TripleTimeBlocks.coefficient_le line 50
7. theorem OAI.SK.Analytic.TripleTimeBlocks.pressure_trial line 65
8. theorem OAI.SK.Analytic.tripleConstrainedPressure_quantile_trial line 86