OAI/Probability/ParisiFinite/LogMean.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Log Mean.

  1. def OAI.ParisiFinite.logMean line 55
  2. def OAI.ParisiFinite.step line 60
  3. def OAI.ParisiFinite.terminal line 64
  4. lemma OAI.ParisiFinite.integral_exp_pos line 66
  5. lemma OAI.ParisiFinite.logMean_zero line 77
  6. lemma OAI.ParisiFinite.logMean_const line 80
  7. lemma OAI.ParisiFinite.logMean_add_const line 86
  8. lemma OAI.ParisiFinite.logMean_mono line 99
  9. lemma OAI.ParisiFinite.integrable_exp_abs line 114
  10. lemma OAI.ParisiFinite.shift_norm_le line 129
  11. lemma OAI.ParisiFinite.integrable_shift line 137
  12. lemma OAI.ParisiFinite.integrable_exp_shift line 145
  13. lemma OAI.ParisiFinite.step_integrals line 161
  14. lemma OAI.ParisiFinite.logMean_le_add line 169
  15. lemma OAI.ParisiFinite.logMean_stable line 180
  16. lemma OAI.ParisiFinite.step_lipschitz line 199
  17. lemma OAI.ParisiFinite.hasDerivAt_terminal line 210
  18. lemma OAI.ParisiFinite.terminal_lipschitz line 224
  19. lemma OAI.ParisiFinite.step_zero_width line 230
  20. lemma OAI.ParisiFinite.terminal_zero line 234
  21. lemma OAI.ParisiFinite.terminal_even line 237
  22. lemma OAI.ParisiFinite.integral_exp_linear line 240
  23. lemma OAI.ParisiFinite.exp_terminal line 246
  24. lemma OAI.ParisiFinite.exp_terminal_shift line 253
  25. lemma OAI.ParisiFinite.integral_exp_terminal line 263
  26. lemma OAI.ParisiFinite.step_terminal line 275
  27. abbrev OAI.ParisiFinite.Schedule line 286
  28. def OAI.ParisiFinite.recursion line 289
  29. def OAI.ParisiFinite.penalty line 294
  30. def OAI.ParisiFinite.width line 298
  31. def OAI.ParisiFinite.Admissible line 301
  32. def OAI.ParisiFinite.functional line 304
  33. lemma OAI.ParisiFinite.recursion_lipschitz line 306
  34. lemma OAI.ParisiFinite.recursion_integrals line 312
  35. lemma OAI.ParisiFinite.step_add_const line 326
  36. lemma OAI.ParisiFinite.step_mean line 330
  37. def OAI.ParisiFinite.replicaSymmetricSchedule line 334
  38. lemma OAI.ParisiFinite.replicaSymmetric_admissible line 337
  39. lemma OAI.ParisiFinite.replicaSymmetric_recursion line 341
  40. lemma OAI.ParisiFinite.replicaSymmetric_penalty line 354
  41. lemma OAI.ParisiFinite.replicaSymmetric_functional line 360
  42. lemma OAI.ParisiInterpolation.memLp_coordinate line 380
  43. lemma OAI.ParisiInterpolation.covariance_coordinate line 385
  44. lemma OAI.ParisiInterpolation.covariance_field line 407
  45. lemma OAI.ParisiInterpolation.hamiltonian_covariance line 428
  46. def OAI.ParisiInterpolation.overlap line 436
  47. lemma OAI.ParisiInterpolation.normalized_hamiltonian_covariance line 438
  48. def OAI.ParisiInterpolation.rotate line 457
  49. def OAI.ParisiInterpolation.increment line 460
  50. def OAI.ParisiInterpolation.expected line 463
  51. lemma OAI.ParisiInterpolation.hasDerivAt_expected_rotate line 468
  52. lemma OAI.ParisiInterpolation.continuous_field line 510
  53. lemma OAI.ParisiInterpolation.integrable_weight_pair line 514
  54. def OAI.ParisiInterpolation.replicaAverage line 526
  55. lemma OAI.ParisiInterpolation.integrable_replicaAverage line 529
  56. lemma OAI.ParisiInterpolation.replicaAverage_const line 535
  57. lemma OAI.ParisiInterpolation.replicaAverage_sub line 540
  58. lemma OAI.ParisiInterpolation.replicaAverage_const_mul line 546
  59. lemma OAI.ParisiInterpolation.replicaAverage_nonneg line 555
  60. def OAI.ParisiInterpolation.replicaMean line 560
  61. lemma OAI.ParisiInterpolation.replicaMean_const line 563
  62. lemma OAI.ParisiInterpolation.replicaMean_sub line 567
  63. lemma OAI.ParisiInterpolation.replicaMean_const_mul line 573
  64. lemma OAI.ParisiInterpolation.replicaMean_nonneg line 577
  65. lemma OAI.ParisiInterpolation.hasDerivAt_expected_rotate_mean line 581
  66. def OAI.ParisiInterpolation.siteCoeff line 605
  67. def OAI.ParisiInterpolation.siteLift line 610
  68. def OAI.ParisiInterpolation.skLift line 613
  69. lemma OAI.ParisiInterpolation.lifts_orthogonal line 616
  70. lemma OAI.ParisiInterpolation.spin_increment line 620
  71. lemma OAI.ParisiInterpolation.siteCoeff_increment line 628
  72. lemma OAI.ParisiInterpolation.siteLift_increment line 634
  73. lemma OAI.ParisiInterpolation.skLift_increment line 640
  74. lemma OAI.ParisiInterpolation.interpolation_increment line 646
  75. def OAI.ParisiInterpolation.interpolatedPressure line 658
  76. def OAI.ParisiInterpolation.remainder line 663
  77. lemma OAI.ParisiInterpolation.remainder_nonneg line 667
  78. lemma OAI.ParisiInterpolation.hasDerivAt_interpolatedPressure line 670