OAI/Probability/SKFluctuations/CavityRow.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Cavity Row.

  1. def OAI.SKFluctuations.Cavity.oldEdge line 22
  2. def OAI.SKFluctuations.Cavity.rowEdge line 26
  3. def OAI.SKFluctuations.Cavity.joinEdge line 29
  4. theorem OAI.SKFluctuations.Cavity.joinEdge_injective line 33
  5. theorem OAI.SKFluctuations.Cavity.joinEdge_surjective line 57
  6. def OAI.SKFluctuations.Cavity.edgeEquiv line 75
  7. theorem OAI.SKFluctuations.Cavity.sum_edges line 78
  8. def OAI.SKFluctuations.Cavity.restDisorder line 84
  9. def OAI.SKFluctuations.Cavity.rowDisorder line 85
  10. def OAI.SKFluctuations.Cavity.restSpin line 86
  11. def OAI.SKFluctuations.Cavity.rowField line 88
  12. def OAI.SKFluctuations.Cavity.restHamiltonian line 92
  13. theorem OAI.SKFluctuations.Cavity.hamiltonian_one_site line 96
  14. def OAI.SKFluctuations.Cavity.restBeta line 110
  15. theorem OAI.SKFluctuations.Cavity.restHamiltonian_eq line 112
  16. theorem OAI.SKFluctuations.Cavity.disorderLaw_one_site line 121
  17. def OAI.SKFluctuations.Cavity.joinSpin line 132
  18. theorem OAI.SKFluctuations.Cavity.joinSpin_old line 135
  19. theorem OAI.SKFluctuations.Cavity.joinSpin_last line 138
  20. def OAI.SKFluctuations.Cavity.spinEquiv line 141
  21. theorem OAI.SKFluctuations.Cavity.sum_spins line 149
  22. theorem OAI.SKFluctuations.Cavity.partitionFunction_one_site line 159
  23. def OAI.SKFluctuations.Cavity.deletedOverlap line 181
  24. theorem OAI.SKFluctuations.Cavity.deletedOverlap_eq line 184
  25. theorem OAI.SKFluctuations.Cavity.deletedOverlap_self line 191
  26. theorem OAI.SKFluctuations.Cavity.abs_deletedOverlap_sub line 195
  27. def OAI.SKFluctuations.Cavity.rowInteractionCoefficient line 207
  28. theorem OAI.SKFluctuations.Cavity.rowInteraction_covariance line 210
  29. def OAI.SKFluctuations.Cavity.actualRowClock line 231
  30. theorem OAI.SKFluctuations.Cavity.actualRowClock_error line 234
  31. theorem OAI.SKFluctuations.Cavity.actualRowClock_error_full line 239
  32. theorem OAI.SKFluctuations.Cavity.actualRow_diagonal line 246
  33. abbrev OAI.SKFluctuations.Cavity.RowCoordinate line 253
  34. def OAI.SKFluctuations.Cavity.mixedCoefficient line 255
  35. def OAI.SKFluctuations.Cavity.mixedVariance line 261
  36. theorem OAI.SKFluctuations.Cavity.mixedVariance_nonneg line 266
  37. def OAI.SKFluctuations.Cavity.mixedVarianceNN line 276
  38. theorem OAI.SKFluctuations.Cavity.mixedVarianceNN_coe line 279
  39. def OAI.SKFluctuations.Cavity.mixedRowClock line 285
  40. theorem OAI.SKFluctuations.Cavity.mixedRow_covariance line 288
  41. theorem OAI.SKFluctuations.Cavity.mixedRowClock_zero line 298
  42. theorem OAI.SKFluctuations.Cavity.mixedRowClock_one line 301
  43. theorem OAI.SKFluctuations.Cavity.mixedRowClock_full_path line 305
  44. theorem OAI.SKFluctuations.Cavity.mixedRow_covariance_posSemidefinite line 313
  45. def OAI.SKFluctuations.Cavity.relocatedClock line 353
  46. theorem OAI.SKFluctuations.Cavity.relocatedClock_monotone line 356
  47. theorem OAI.SKFluctuations.Cavity.relocatedClock_nonneg line 367
  48. theorem OAI.SKFluctuations.Cavity.relocatedClock_le line 374
  49. theorem OAI.SKFluctuations.Cavity.relocatedClock_one line 381
  50. theorem OAI.SKFluctuations.Cavity.relocated_mixedRowClock line 388
  51. theorem OAI.SKFluctuations.Cavity.relocatedRow_hasDerivAt_t line 398
  52. theorem OAI.SKFluctuations.Cavity.relocatedRow_hasDerivAt_l line 413
  53. theorem OAI.SKFluctuations.Cavity.mixedVariance_monotone line 427
  54. theorem OAI.SKFluctuations.Cavity.scalarClock_monotone line 439
  55. def OAI.SKFluctuations.Cavity.relocatedVariance line 448
  56. theorem OAI.SKFluctuations.Cavity.relocatedVariance_monotone line 452
  57. theorem OAI.SKFluctuations.Cavity.relocatedVariance_increment_nonneg line 460
  58. theorem OAI.SKFluctuations.Cavity.relocatedRow_covariance line 469
  59. theorem OAI.SKFluctuations.Cavity.relocatedVariance_at_cut line 492