OAI/Probability/SKFluctuations/CavityActualEndpoint.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Cavity Actual Endpoint.

  1. abbrev OAI.SKFluctuations.Cavity.RestCoordinate line 21
  2. abbrev OAI.SKFluctuations.Cavity.ActiveCoordinate line 22
  3. abbrev OAI.SKFluctuations.Cavity.DormantCoordinate line 23
  4. abbrev OAI.SKFluctuations.Cavity.FullCoordinate line 24
  5. def OAI.SKFluctuations.Cavity.restCoefficient line 26
  6. def OAI.SKFluctuations.Cavity.restFeature line 30
  7. def OAI.SKFluctuations.Cavity.dormantCoefficient line 33
  8. def OAI.SKFluctuations.Cavity.dormantFeature line 37
  9. def OAI.SKFluctuations.Cavity.fullFeature line 42
  10. def OAI.SKFluctuations.Cavity.restWeight line 46
  11. def OAI.SKFluctuations.Cavity.fullWeight line 47
  12. theorem OAI.SKFluctuations.Cavity.restWeight_pos line 49
  13. theorem OAI.SKFluctuations.Cavity.fullWeight_eq line 53
  14. theorem OAI.SKFluctuations.Cavity.restFeature_apply line 58
  15. theorem OAI.SKFluctuations.Cavity.dormantFeature_apply line 62
  16. theorem OAI.SKFluctuations.Cavity.fullFeature_apply line 66
  17. theorem OAI.SKFluctuations.Cavity.fullFeature_restrict line 73
  18. def OAI.SKFluctuations.Cavity.fullVariance line 82
  19. theorem OAI.SKFluctuations.Cavity.fullVariance_nonneg line 86
  20. def OAI.SKFluctuations.Cavity.fullVarianceNN line 97
  21. theorem OAI.SKFluctuations.Cavity.fullVarianceNN_zero line 100
  22. theorem OAI.SKFluctuations.Cavity.fullHierarchy_scalar_endpoint line 107
  23. theorem OAI.SKFluctuations.Cavity.fullReplica_scalar_endpoint line 121
  24. def OAI.SKFluctuations.Cavity.originalDisorderPoint line 141
  25. theorem OAI.SKFluctuations.Cavity.fullFeature_originalDisorderPoint line 148
  26. theorem OAI.SKFluctuations.Cavity.fullPartition_originalDisorderPoint line 173
  27. theorem OAI.SKFluctuations.Cavity.fullLogPartition_originalDisorderPoint line 184
  28. def OAI.SKFluctuations.Hierarchy.ReplicaTree.assignmentGauge line 203
  29. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.weight_gauge line 211
  30. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_gauge line 236
  31. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_gauge_odd line 251
  32. def OAI.SKFluctuations.Cavity.rowSpinFlip line 273
  33. theorem OAI.SKFluctuations.Cavity.rowSpinFlip_apply line 276
  34. theorem OAI.SKFluctuations.Cavity.spinValue_not line 279
  35. def OAI.SKFluctuations.Cavity.rowDriverSign line 283
  36. theorem OAI.SKFluctuations.Cavity.rowDriverSign_sq line 286
  37. def OAI.SKFluctuations.Cavity.rowDriverFlip line 290
  38. theorem OAI.SKFluctuations.Cavity.fullWeight_rowSpinFlip line 293
  39. theorem OAI.SKFluctuations.Cavity.fullFeature_rowFlip line 298
  40. theorem OAI.SKFluctuations.Cavity.rowDriverFlip_gaussian line 309
  41. theorem OAI.SKFluctuations.Cavity.rowDriverFlip_fixed line 315
  42. theorem OAI.SKFluctuations.Cavity.actualRow_odd_block line 323
  43. def OAI.SKFluctuations.Cavity.fullCoefficient line 344
  44. theorem OAI.SKFluctuations.Cavity.scalarFeature_apply_spin line 348
  45. theorem OAI.SKFluctuations.Cavity.fullFeature_single line 352
  46. def OAI.SKFluctuations.Cavity.fullAmplitude line 365
  47. theorem OAI.SKFluctuations.Cavity.fullAmplitude_nonneg line 369
  48. theorem OAI.SKFluctuations.Cavity.fullFeature_abs line 372
  49. theorem OAI.SKFluctuations.Cavity.fullFeature_square line 379
  50. theorem OAI.SKFluctuations.Cavity.fullWeight_pos line 383
  51. def OAI.SKFluctuations.Cavity.rowChangeBound line 389
  52. theorem OAI.SKFluctuations.Cavity.rowChangeBound_nonneg line 392
  53. theorem OAI.SKFluctuations.Cavity.rowChangeBound_cost line 396
  54. theorem OAI.SKFluctuations.Cavity.rowChangeBound_cost_le line 407
  55. theorem OAI.SKFluctuations.Cavity.fullVariance_monotone line 413
  56. theorem OAI.SKFluctuations.Cavity.actualRow_disorderWeight_close line 426
  57. theorem OAI.SKFluctuations.Cavity.actualRow_disorderExpect_close line 447
  58. def OAI.SKFluctuations.Cavity.cavityPath line 463
  59. theorem OAI.SKFluctuations.Cavity.cavityPath_monotone line 468
  60. theorem OAI.SKFluctuations.Cavity.cavityPath_nonneg line 477
  61. theorem OAI.SKFluctuations.Cavity.cavityPath_row_bound line 485
  62. theorem OAI.SKFluctuations.Cavity.cavityPath_sub_bound line 502
  63. theorem OAI.SKFluctuations.Cavity.cavityPath_expect_close line 522
  64. theorem OAI.SKFluctuations.Hierarchy.levelPairMean_product_le_succ line 557
  65. theorem OAI.SKFluctuations.Hierarchy.levelPairMean_product_monotone line 585
  66. theorem OAI.SKFluctuations.Hierarchy.levelPairMean_sum line 591
  67. theorem OAI.SKFluctuations.Hierarchy.levelPairMean_const_mul line 607
  68. theorem OAI.SKFluctuations.levelPairMean_overlap_monotone line 622
  69. theorem OAI.SKFluctuations.rootLevelPairMean_overlap_monotone line 638