OAI/Probability/DilutedSpin/CavitySeparable.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DilutedSpinGlass.cavityArrayEnergy line 15
  2. lemma OAI.DilutedSpinGlass.measurable_cavityArrayEnergy line 21
  3. def OAI.DilutedSpinGlass.cavityArrayValue line 37
  4. lemma OAI.DilutedSpinGlass.measurable_cavityArrayValue line 43
  5. lemma OAI.DilutedSpinGlass.cavityArrayValue_bound line 53
  6. lemma OAI.DilutedSpinGlass.PrescribedTree.path_proj_fst line 80
  7. lemma OAI.DilutedSpinGlass.PrescribedTree.path_proj_join line 89
  8. def OAI.DilutedSpinGlass.PrescribedTree.singleBlockEnergy line 97
  9. def OAI.DilutedSpinGlass.PrescribedTree.allocatedEnergy line 105
  10. lemma OAI.DilutedSpinGlass.PrescribedTree.cavityEnergy_join line 115
  11. lemma OAI.DilutedSpinGlass.PrescribedTree.cavityRoot_separable line 145