OAI/Probability/ParisiFinite/Average.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

Average.

  1. def OAI.SKCavity.average line 60
  2. lemma OAI.SKCavity.average_pos line 62
  3. lemma OAI.SKCavity.partition_mul_average line 66
  4. lemma OAI.SKCavity.log_average_exp line 75
  5. lemma OAI.SKCavity.restrictLeft_snoc line 85
  6. def OAI.SKCavity.extend line 92
  7. lemma OAI.SKCavity.partition_extend line 95
  8. lemma OAI.SKCavity.logPartition_extend line 108
  9. def OAI.SKCavity.site line 115
  10. def OAI.SKCavity.core line 118
  11. def OAI.SKCavity.correctionField line 121
  12. lemma OAI.SKCavity.field_cavityCoeff line 124
  13. lemma OAI.SKCavity.field_correctedCoeff line 132
  14. lemma OAI.SKCavity.extend_scale line 140
  15. def OAI.SKCavity.cavityLog line 147
  16. def OAI.SKCavity.correctionLog line 152
  17. lemma OAI.SKCavity.cavityLog_sub line 156
  18. lemma OAI.SKCavity.correctionLog_sub line 162
  19. def OAI.SKCavity.coreLift line 178
  20. lemma OAI.SKCavity.field_coreLift line 181
  21. lemma OAI.SKCavity.integrable_coreLift line 190
  22. lemma OAI.SKCavity.expected_coreLift line 196
  23. lemma OAI.SKCavity.integrable_cavityLog line 206
  24. lemma OAI.SKCavity.integrable_correctionLog line 213
  25. lemma OAI.SKCavity.expected_cavityLog line 220
  26. lemma OAI.SKCavity.expected_correctionLog line 227
  27. def OAI.SKCavity.increment line 235
  28. lemma OAI.SKCavity.increment_eq line 240
  29. lemma OAI.SKCavity.increment_lower line 245
  30. lemma OAI.SKCavity.frequently_increment_le_of_slope line 260
  31. lemma OAI.SKCavity.tendsto_pressure_perSpin line 287
  32. lemma OAI.SKCavity.frequently_cavity_upper line 295
  33. lemma OAI.SKCavity.increment_bounded_below line 302
  34. lemma OAI.SKCavity.limitingFreeEnergy_ge_cavity_liminf line 311
  35. def OAI.SKCavity.replicaWeight line 326
  36. lemma OAI.SKCavity.replicaWeight_nonneg line 329
  37. lemma OAI.SKCavity.replicaWeight_le_one line 333
  38. lemma OAI.SKCavity.sum_replicaWeight line 337
  39. lemma OAI.SKCavity.continuous_replicaWeight line 342
  40. def OAI.SKCavity.coreGibbs line 350
  41. lemma OAI.SKCavity.coreGibbs_eq_field line 353
  42. lemma OAI.SKCavity.continuous_coreGibbs line 359
  43. lemma OAI.SKCavity.integrable_replicaWeight line 364
  44. def OAI.SKCavity.replicaMass line 375
  45. lemma OAI.SKCavity.replicaMass_nonneg line 378
  46. lemma OAI.SKCavity.sum_replicaMass line 381
  47. def OAI.SKCavity.finiteProbability line 390
  48. lemma OAI.SKCavity.integral_finiteProbability line 397
  49. def OAI.SKCavity.replicaLaw line 408
  50. lemma OAI.SKCavity.integral_replicaLaw line 411
  51. abbrev OAI.SKCavity.OverlapEntry line 426
  52. abbrev OAI.SKCavity.OverlapArray line 427
  53. lemma OAI.SKCavity.abs_overlap_le_one line 429
  54. lemma OAI.SKCavity.overlap_symm line 439
  55. lemma OAI.SKCavity.overlap_self line 442
  56. def OAI.SKCavity.extendReplicas line 449
  57. lemma OAI.SKCavity.extendReplicas_eq line 452
  58. def OAI.SKCavity.configurationOverlap line 455
  59. def OAI.SKCavity.overlapLaw line 461
  60. lemma OAI.SKCavity.integral_overlapLaw line 465
  61. theorem OAI.SKCavity.exists_overlap_limit line 475
  62. lemma OAI.SKCavity.overlap_quadratic line 489
  63. def OAI.SKCavity.GramArrays line 513
  64. lemma OAI.SKCavity.isClosed_GramArrays line 517
  65. lemma OAI.SKCavity.configurationOverlap_mem_Gram line 524
  66. lemma OAI.SKCavity.finiteProbability_set_of_forall line 532
  67. lemma OAI.SKCavity.overlapLaw_Gram line 540
  68. lemma OAI.SKCavity.overlap_limit_Gram line 544
  69. theorem OAI.SKCavity.exists_Gram_overlap_limit line 555
  70. lemma OAI.SKCavity.tuple_partition line 574
  71. lemma OAI.SKCavity.replicaWeight_eq_weight line 580
  72. def OAI.SKCavity.tupleCoeff line 586
  73. lemma OAI.SKCavity.linearField_tupleCoeff line 590
  74. lemma OAI.SKCavity.replicaWeight_tupleCoeff line 596
  75. lemma OAI.SKCavity.integrable_linear_replicaWeight line 603
  76. lemma OAI.SKCavity.integrable_coord_replicaWeight line 608
  77. lemma OAI.SKCavity.integral_coord_replicaWeight line 616
  78. lemma OAI.GaussianConcentration.memLp_lipschitz line 635
  79. lemma OAI.GaussianConcentration.memLp_standard_id line 647
  80. lemma OAI.GaussianConcentration.standard_second_moment line 653
  81. lemma OAI.GaussianConcentration.variance_lipschitz_real line 660
  82. def OAI.GaussianConcentration.CoordinateLipschitz line 678
  83. lemma OAI.GaussianConcentration.CoordinateLipschitz.lipschitz line 681
  84. lemma OAI.GaussianConcentration.CoordinateLipschitz.memLp line 694