OAI/Probability/SKBarriers/Parisi/QuantileLipschitz.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.extendedQuantileParisi_lipschitz_positive line 16
  2. def OAI.SK.Analytic.strictQuantile line 65
  3. theorem OAI.SK.Analytic.strictQuantile_gap line 67
  4. theorem OAI.SK.Analytic.strictQuantile_mem line 74
  5. def OAI.SK.Analytic.regularizeQuantile line 82
  6. theorem OAI.SK.Analytic.regularizeQuantile_positive line 85
  7. theorem OAI.SK.Analytic.regularizeQuantile_mem line 92
  8. theorem OAI.SK.Analytic.regularizeQuantile_tendsto line 103
  9. theorem OAI.SK.Analytic.extendedQuantileParisi_lipschitz line 110