OAI/Probability/ParisiFinite/DyadicMeshTendsto.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Dyadic Mesh Tendsto.

  1. lemma OAI.ParisiFinite.dyadicMesh_tendsto line 63
  2. lemma OAI.ParisiFinite.dyadicMesh_le line 70
  3. lemma OAI.ParisiFinite.gaussianSmallError_dyadic_tendsto line 74
  4. def OAI.ParisiFinite.dyadicEvolution line 91
  5. lemma OAI.ParisiFinite.dyadic_low_monotone line 94
  6. lemma OAI.ParisiFinite.dyadic_high_antitone line 99
  7. lemma OAI.ParisiFinite.dyadic_low_bddAbove line 104
  8. lemma OAI.ParisiFinite.dyadic_low_tendsto line 111
  9. lemma OAI.ParisiFinite.dyadic_high_tendsto line 117
  10. lemma OAI.ParisiFinite.dyadicEvolution_lipschitz line 132
  11. def OAI.ParisiFinite.uniformLower line 148
  12. lemma OAI.ParisiFinite.dyadicSchedule_eq_uniform line 151
  13. lemma OAI.ParisiFinite.width_append line 186
  14. lemma OAI.ParisiFinite.width_cons line 187
  15. lemma OAI.ParisiFinite.penalty_append line 188
  16. lemma OAI.ParisiFinite.dyadicSchedule_width line 196
  17. lemma OAI.ParisiFinite.dyadic_penalty_succ line 202
  18. def OAI.ParisiFinite.coefficientPenalty line 209
  19. lemma OAI.ParisiFinite.coefficient_integrable line 212
  20. lemma OAI.ParisiFinite.coefficientPenalty_split line 218
  21. lemma OAI.ParisiFinite.constant_coefficient_integral line 225
  22. lemma OAI.ParisiFinite.coefficientPenalty_base_bounds line 230
  23. lemma OAI.ParisiFinite.dyadic_penalty_bounds line 246
  24. lemma OAI.ParisiFinite.dyadic_penalty_difference line 264
  25. lemma OAI.ParisiFinite.dyadic_penalty_error line 293
  26. lemma OAI.ParisiFinite.dyadic_penalty_tendsto line 307
  27. def OAI.ParisiFinite.orderParameterFunctional line 329
  28. lemma OAI.ParisiFinite.dyadic_admissible line 332
  29. lemma OAI.ParisiFinite.dyadic_functional_tendsto line 346
  30. lemma OAI.ParisiFinite.limitingFreeEnergy_le_orderParameterFunctional line 354
  31. def OAI.SKCavity.overlapCDFCoefficient line 367
  32. lemma OAI.SKCavity.overlapCDFCoefficient_mono line 370
  33. lemma OAI.SKCavity.overlapCDFCoefficient_bound line 375
  34. lemma OAI.SKCavity.dyadic_CDF_schedule line 381
  35. abbrev OAI.ParisiFinite.OrderPoint line 402
  36. def OAI.ParisiFinite.measureCoefficient line 405
  37. def OAI.ParisiFinite.measureFunctional line 408
  38. lemma OAI.ParisiFinite.measureCoefficient_mono line 411
  39. lemma OAI.ParisiFinite.measureCoefficient_bound line 422
  40. lemma OAI.ParisiFinite.pressure_le_measureFunctional line 429
  41. def OAI.SKCavity.orderPointOfArray line 437
  42. lemma OAI.SKCavity.orderPointOfArray_continuous line 440
  43. def OAI.SKCavity.orderParameterLaw line 444
  44. lemma OAI.SKCavity.orderParameterLaw_coefficient line 447
  45. lemma OAI.SKCavity.dyadic_indices_tendsto line 463
  46. theorem OAI.SKCavity.exists_measure_pressure_equality line 475
  47. def OAI.ParisiFinite.IsMinimizingParisiMeasure line 507
  48. theorem OAI.ParisiFinite.exists_minimizing_Parisi_measure line 512
  49. lemma OAI.ParisiFinite.tiltedMean_const line 526
  50. lemma OAI.ParisiFinite.tiltedMean_nonneg line 532
  51. lemma OAI.ParisiFinite.tiltedMean_mono line 538
  52. lemma OAI.ParisiFinite.tiltedMean_variance_nonneg line 546
  53. def OAI.ParisiFinite.HasParisiCurvature line 576
  54. lemma OAI.ParisiFinite.terminal_hasParisiCurvature line 579
  55. lemma OAI.ParisiFinite.transform_hasParisiCurvature line 589
  56. lemma OAI.ParisiFinite.smoothRecursion_hasParisiCurvature line 619
  57. lemma OAI.ParisiFinite.curvature_abs_d2 line 635
  58. lemma OAI.ParisiFinite.curvature_gradient_lipschitz line 641
  59. lemma OAI.ParisiFinite.curvature_taylor_error line 648
  60. lemma OAI.ParisiFinite.curvature_derivative_stability line 666
  61. lemma OAI.ParisiFinite.uniform_derivative_cauchy line 678
  62. lemma OAI.ParisiFinite.exists_uniform_derivative_limit line 706