OAI/Probability/ParisiFinite/OverlapDiscountMono.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Overlap Discount Mono.

  1. lemma OAI.SKCavity.overlapDiscount_mono line 64
  2. lemma OAI.SKCavity.overlapDiscount_le_one line 68
  3. lemma OAI.SKCavity.uniform_schedule_penalty line 72
  4. def OAI.SKCavity.gridSchedule line 86
  5. lemma OAI.SKCavity.gridSchedule_admissible line 91
  6. lemma OAI.SKCavity.gridSchedule_penalty line 110
  7. theorem OAI.SKCavity.gridCavityMixture_tendsto line 134
  8. lemma OAI.SKCavity.quadratic_indices_tendsto line 190
  9. theorem OAI.SKCavity.gridFunctional_cavity_error line 195
  10. theorem OAI.ParisiGuerra.exists_admissible_schedule_sequence line 217
  11. def OAI.ParisiGuerra.finiteParisiValues line 242
  12. def OAI.ParisiGuerra.finiteParisiInfimum line 245
  13. lemma OAI.ParisiGuerra.finiteParisiValues_nonempty line 247
  14. lemma OAI.ParisiGuerra.finiteParisiValues_bddBelow line 252
  15. theorem OAI.ParisiGuerra.limitingFreeEnergy_eq_finiteParisiInfimum line 262
  16. lemma OAI.ParisiGuerra.exists_admissible_functional_lt line 274
  17. lemma OAI.ParisiFinite.logMean_expectation_le line 286
  18. lemma OAI.ParisiFinite.logMean_parameter_mono line 301
  19. lemma OAI.ParisiFinite.step_parameter_mono line 335
  20. lemma OAI.ParisiFinite.step_le_of_le line 341
  21. lemma OAI.ParisiFinite.step_stable line 347
  22. def OAI.ParisiFinite.gaussianSmallError line 359
  23. lemma OAI.ParisiFinite.abs_scaled_lipschitz line 362
  24. lemma OAI.ParisiFinite.gaussianSmallError_nonneg line 369
  25. lemma OAI.ParisiFinite.step_id_error line 380
  26. lemma OAI.ParisiFinite.gaussianSmallError_grid_tendsto line 406
  27. lemma OAI.ParisiFinite.gaussian_pair_sum_map line 429
  28. lemma OAI.ParisiFinite.gaussian_pair_integrable line 462
  29. lemma OAI.ParisiFinite.gaussian_pair_integral line 470
  30. lemma OAI.ParisiFinite.exp_step line 477
  31. lemma OAI.ParisiFinite.step_semigroup line 483
  32. def OAI.ParisiFinite.evolve line 514
  33. lemma OAI.ParisiFinite.evolve_lipschitz line 518
  34. lemma OAI.ParisiFinite.recursion_eq_evolve line 524
  35. lemma OAI.ParisiFinite.evolve_append line 529
  36. lemma OAI.ParisiFinite.evolve_stable line 535
  37. lemma OAI.ParisiFinite.evolve_mono line 543
  38. lemma OAI.ParisiFinite.evolve_shift_error line 553
  39. lemma OAI.ParisiFinite.evolve_split line 570
  40. def OAI.ParisiFinite.dyadicSchedule line 586
  41. def OAI.ParisiFinite.dyadicMesh line 590
  42. lemma OAI.ParisiFinite.dyadicMesh_succ line 592
  43. lemma OAI.ParisiFinite.dyadicSchedule_nonempty line 597
  44. lemma OAI.ParisiFinite.dyadicSchedule_shift line 605
  45. lemma OAI.ParisiFinite.dyadicSchedule_grid_error line 616
  46. lemma OAI.ParisiFinite.dyadicSchedule_low_le_high line 631
  47. lemma OAI.ParisiFinite.dyadicSchedule_low_refine line 643
  48. lemma OAI.ParisiFinite.dyadicSchedule_high_refine line 664