OAI/Probability/SKBarriers/Parisi/QuantileClamp.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.cumulativeGapMap_nonneg_iff line 15
2. def OAI.SK.Analytic.clampQuantile line 25
3. theorem OAI.SK.Analytic.clampQuantile_gap line 27
4. theorem OAI.SK.Analytic.clampQuantile_admissible line 46
5. theorem OAI.SK.Analytic.extendedQuantileParisi_clamp_le line 52
6. theorem OAI.SK.Analytic.exists_admissible_scalar_lower_bound line 83