OAI/Probability/ParisiFinite/BoundedOf.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

Bounded Of.

  1. def OAI.ParisiFinite.boundedOf line 59
  2. lemma OAI.ParisiFinite.bounded_abs line 69
  3. def OAI.ParisiFinite.tiltMap line 74
  4. lemma OAI.ParisiFinite.tiltMap_apply line 86
  5. lemma OAI.ParisiFinite.tiltMap_mono line 90
  6. lemma OAI.ParisiFinite.tiltMap_const line 95
  7. lemma OAI.ParisiFinite.tiltMap_nonneg line 100
  8. lemma OAI.ParisiFinite.norm_tiltMap_le line 106
  9. def OAI.ParisiFinite.DirectionalField.firstBCF line 114
  10. def OAI.ParisiFinite.DirectionalField.secondBCF line 117
  11. lemma OAI.ParisiFinite.DirectionalField.firstBCF_apply line 120
  12. lemma OAI.ParisiFinite.DirectionalField.secondBCF_apply line 121
  13. lemma OAI.ParisiFinite.DirectionalField.firstBCF_transform line 123
  14. lemma OAI.ParisiFinite.DirectionalField.secondBCF_transform line 126
  15. def OAI.ParisiFinite.FieldFamily.dotBCF line 134
  16. lemma OAI.ParisiFinite.FieldFamily.dotBCF_apply line 137
  17. lemma OAI.ParisiFinite.FieldFamily.dotBCF_constant line 139
  18. lemma OAI.ParisiFinite.FieldFamily.dotBCF_transform line 141
  19. def OAI.ParisiFinite.transport line 160
  20. lemma OAI.ParisiFinite.transport_nonneg line 166
  21. lemma OAI.ParisiFinite.transport_const line 173
  22. lemma OAI.ParisiFinite.hierarchy_firstBCF line 179
  23. def OAI.ParisiFinite.gibbsMap line 193
  24. lemma OAI.ParisiFinite.gibbsMap_apply line 203
  25. lemma OAI.ParisiFinite.gibbsMap_nonneg line 205
  26. lemma OAI.ParisiFinite.gibbsMap_const line 210
  27. def OAI.ParisiFinite.spinObserve line 218
  28. lemma OAI.ParisiFinite.spinObserve_nonneg line 222
  29. lemma OAI.ParisiFinite.spinObserve_const line 226
  30. lemma OAI.ParisiFinite.spin_first_observe line 230
  31. def OAI.ParisiFinite.spinWeight line 235
  32. lemma OAI.ParisiFinite.spinWeight_nonneg line 239
  33. lemma OAI.ParisiFinite.spinObserve_eq_sum line 246
  34. lemma OAI.ParisiFinite.sum_spinWeight line 255
  35. abbrev OAI.ParisiFinite.Noise line 273
  36. def OAI.ParisiFinite.noiseGradient line 275
  37. def OAI.ParisiFinite.noiseHessian line 279
  38. def OAI.ParisiFinite.noiseResponse line 283
  39. lemma OAI.ParisiFinite.noiseResponse_nil line 286
  40. lemma OAI.ParisiFinite.noiseResponse_cons line 289
  41. lemma OAI.ParisiFinite.noiseHessian_transform line 294
  42. lemma OAI.ParisiFinite.noiseResponse_transform line 306
  43. def OAI.ParisiFinite.coordinateNoise line 312
  44. def OAI.ParisiFinite.allNoise line 314
  45. lemma OAI.ParisiFinite.hierarchy_local_sum line 318
  46. def OAI.ParisiFinite.hierarchyRemainder line 339
  47. def OAI.ParisiFinite.diagonalNoise line 349
  48. lemma OAI.ParisiFinite.trace_firstBCF line 353
  49. lemma OAI.ParisiFinite.trace_secondBCF line 356
  50. lemma OAI.ParisiFinite.trace_noiseResponse line 365
  51. lemma OAI.ParisiFinite.hierarchy_sum_rule line 379
  52. lemma OAI.ParisiFinite.hierarchy_derivative_sum_rule line 396
  53. def OAI.ParisiFinite.replicaObserve line 418
  54. lemma OAI.ParisiFinite.replicaObserve_apply line 424
  55. lemma OAI.ParisiFinite.sum_spinWeight_apply line 429
  56. lemma OAI.ParisiFinite.replicaObserve_nonneg line 433
  57. lemma OAI.ParisiFinite.replicaObserve_const line 440
  58. lemma OAI.ParisiFinite.replicaObserve_rankOne line 446
  59. def OAI.ParisiFinite.kernelNoise line 462
  60. lemma OAI.ParisiFinite.kernelNoise_diagonal line 467
  61. lemma OAI.ParisiFinite.noiseGradient_replica line 474
  62. lemma OAI.ParisiFinite.replicaObserve_ge_const line 487
  63. def OAI.ParisiFinite.prefixTransport line 503
  64. lemma OAI.ParisiFinite.prefixTransport_const line 510
  65. lemma OAI.ParisiFinite.prefixTransport_nonneg line 516
  66. lemma OAI.ParisiFinite.transport_append line 523
  67. lemma OAI.ParisiFinite.allNoise_append line 531
  68. lemma OAI.ParisiFinite.remainder_constant_prefix line 539
  69. lemma OAI.ParisiFinite.remainder_nonempty_constant_prefix line 552
  70. def OAI.ParisiFinite.coordinatesKernel line 572
  71. lemma OAI.ParisiFinite.coordinatesKernel_nil line 575
  72. lemma OAI.ParisiFinite.coordinatesKernel_cons line 577
  73. lemma OAI.ParisiFinite.coordinatesKernel_append line 580
  74. lemma OAI.ParisiFinite.coordinatesKernel_ofFn line 584
  75. lemma OAI.ParisiFinite.kernelNoise_allNoise line 588
  76. def OAI.ParisiFinite.dummyCoordinate line 601
  77. lemma OAI.ParisiFinite.coordinatesKernel_dummy line 603
  78. def OAI.ParisiGuerra.costBlock line 612
  79. def OAI.ParisiGuerra.siteBlock line 616
  80. def OAI.ParisiGuerra.siteCoordinates line 620
  81. def OAI.ParisiGuerra.coordinates line 623
  82. def OAI.ParisiGuerra.pressureCurve line 625
  83. lemma OAI.ParisiGuerra.costBlock_gamma line 628
  84. lemma OAI.ParisiGuerra.siteBlock_gamma line 633
  85. lemma OAI.ParisiGuerra.costBlock_kernel line 638
  86. lemma OAI.ParisiGuerra.siteBlock_kernel line 647
  87. def OAI.ParisiGuerra.frontierKernel line 661
  88. lemma OAI.ParisiGuerra.costBlock_frontier line 664
  89. lemma OAI.ParisiGuerra.frontier_add_site line 673