OAI/Probability/ParisiFinite/PartitionSite.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Partition Site.

  1. lemma OAI.ParisiInterpolation.partition_site line 56
  2. lemma OAI.ParisiInterpolation.logPartition_site line 68
  3. lemma OAI.ParisiInterpolation.siteCoeff_field line 74
  4. lemma OAI.ParisiInterpolation.logPartition_siteCoeff line 82
  5. lemma OAI.ParisiInterpolation.log_cosh_integrable line 87
  6. lemma OAI.ParisiInterpolation.expected_siteCoeff line 95
  7. lemma OAI.ParisiInterpolation.interpolatedPressure_zero line 116
  8. lemma OAI.ParisiInterpolation.interpolatedPressure_pi_div_two line 128
  9. lemma OAI.ParisiInterpolation.norm_replicaAverage_le line 151
  10. lemma OAI.ParisiInterpolation.continuous_replicaMean_rotate line 166
  11. lemma OAI.ParisiInterpolation.continuous_remainder line 183
  12. lemma OAI.ParisiInterpolation.hasDerivAt_correctedPressure line 188
  13. lemma OAI.ParisiInterpolation.pressure_sum_rule line 200
  14. lemma OAI.ParisiInterpolation.integrated_remainder_nonneg line 214
  15. lemma OAI.ParisiInterpolation.pressure_le_trial line 224
  16. lemma OAI.ParisiInterpolation.freeEnergy_sum_rule line 242
  17. lemma OAI.ParisiInterpolation.freeEnergy_le_functional line 254
  18. lemma OAI.ParisiInterpolation.limitingFreeEnergy_le_functional line 260
  19. structure OAI.ParisiFinite.SmoothField line 276
  20. lemma OAI.ParisiFinite.SmoothField.continuousVal line 290
  21. lemma OAI.ParisiFinite.SmoothField.continuousD1 line 293
  22. lemma OAI.ParisiFinite.SmoothField.lipschitz line 296
  23. lemma OAI.ParisiFinite.SmoothField.lipschitzD1 line 302
  24. lemma OAI.ParisiFinite.exp_shift_near_le line 310
  25. def OAI.ParisiFinite.expMoment line 331
  26. lemma OAI.ParisiFinite.integrable_exp_weight line 334
  27. lemma OAI.ParisiFinite.hasDerivAt_expMoment line 341
  28. def OAI.ParisiFinite.expMass line 386
  29. def OAI.ParisiFinite.tiltedMean line 389
  30. lemma OAI.ParisiFinite.expMass_pos line 392
  31. lemma OAI.ParisiFinite.tiltedMean_zero line 395
  32. lemma OAI.ParisiFinite.abs_tiltedMean_le line 399
  33. lemma OAI.ParisiFinite.hasDerivAt_expMass line 413
  34. lemma OAI.ParisiFinite.hasDerivAt_gaussianAverage line 424
  35. lemma OAI.ParisiFinite.hasDerivAt_step line 441
  36. lemma OAI.ParisiFinite.expMoment_add line 460
  37. lemma OAI.ParisiFinite.expMoment_const_mul line 467
  38. lemma OAI.ParisiFinite.tiltedMean_add line 471
  39. lemma OAI.ParisiFinite.tiltedMean_const_mul line 477
  40. lemma OAI.ParisiFinite.sq_bound line 481
  41. lemma OAI.ParisiFinite.hasDerivAt_tiltedMean_d1 line 486
  42. lemma OAI.ParisiFinite.continuous_expMoment line 513
  43. lemma OAI.ParisiFinite.continuous_tiltedMean line 531
  44. def OAI.ParisiFinite.SmoothField.transform line 546
  45. lemma OAI.ParisiFinite.hasDerivAt_tanh_scaled line 581
  46. def OAI.ParisiFinite.terminalField line 602
  47. def OAI.ParisiFinite.smoothRecursion line 622
  48. lemma OAI.ParisiFinite.smoothRecursion_val line 626
  49. lemma OAI.ParisiFinite.smoothRecursion_bound1 line 635