OAI/Probability/SKBarriers/Parisi/QuantileChain.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.quantileCDF_bounds line 14
2. theorem OAI.SK.Analytic.quantileCDF_monotone line 22
3. theorem OAI.SK.Analytic.monotone_cons_zero_quantiles line 32
4. theorem OAI.SK.Analytic.quantile_knots_gap line 40
5. theorem OAI.SK.Analytic.quantileCDF_on_interval line 46
6. theorem OAI.SK.Analytic.quantile_prefix_chain line 68