OAI/Probability/SKBarriers/Coverage/ThermodynamicLimit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.finiteParisiValues line 16
  2. def OAI.SK.Analytic.finiteParisiInf line 20
  3. def OAI.SK.Analytic.quenchedPressure line 22
  4. theorem OAI.SK.Analytic.finiteParisiValues_nonempty line 25
  5. theorem OAI.SK.Analytic.quenched_le_finiteParisiValue line 30
  6. theorem OAI.SK.Analytic.finiteParisiValues_bddBelow line 36
  7. theorem OAI.SK.Analytic.finiteParisiInf_le line 39
  8. theorem OAI.SK.Analytic.quenched_le_finiteParisiInf line 44
  9. def OAI.SK.Analytic.finiteComparisonError line 48
  10. def OAI.SK.Analytic.finiteComparisonErrorLimit line 52
  11. theorem OAI.SK.Analytic.finiteParisiInf_sub_error_le line 56
  12. theorem OAI.SK.Analytic.finiteComparisonRatio_tendsto line 63
  13. theorem OAI.SK.Analytic.finiteComparisonError_tendsto line 69
  14. theorem OAI.SK.Analytic.finiteComparisonErrorLimit_continuous line 78
  15. theorem OAI.SK.Analytic.eventually_lt_quenched_of_error line 83
  16. theorem OAI.SK.Analytic.eventually_lt_quenched_of_mesh line 94
  17. theorem OAI.SK.Analytic.quenchedPressure_tendsto_finiteParisiInf line 108