OAI/Probability/SKFluctuations/CavityFactorization.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Cavity Factorization.

  1. theorem OAI.SKFluctuations.Hierarchy.shiftedContinuation_prod_add line 27
  2. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_prod_mul line 42
  3. def OAI.SKFluctuations.Hierarchy.sumLeft line 64
  4. def OAI.SKFluctuations.Hierarchy.sumRight line 66
  5. def OAI.SKFluctuations.Hierarchy.productFeature line 69
  6. theorem OAI.SKFluctuations.Hierarchy.productFeature_apply line 74
  7. theorem OAI.SKFluctuations.Hierarchy.spinPartition_product line 80
  8. theorem OAI.SKFluctuations.Hierarchy.spinLogPartition_product line 94
  9. theorem OAI.SKFluctuations.Hierarchy.spinWeight_product line 105
  10. def OAI.SKFluctuations.Hierarchy.leftSteps line 116
  11. def OAI.SKFluctuations.Hierarchy.rightSteps line 118
  12. theorem OAI.SKFluctuations.Hierarchy.OrderedSteps.leftSteps line 122
  13. theorem OAI.SKFluctuations.Hierarchy.OrderedSteps.rightSteps line 131
  14. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_product line 141
  15. theorem OAI.SKFluctuations.Hierarchy.integral_sumGaussian line 180
  16. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_sum_mul line 190
  17. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_product line 214
  18. def OAI.SKFluctuations.Hierarchy.ReplicaTree.cavityLeft line 244
  19. def OAI.SKFluctuations.Hierarchy.ReplicaTree.cavityRight line 251
  20. def OAI.SKFluctuations.Hierarchy.ReplicaTree.cavityAssignment line 259
  21. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.weight_cavity_product line 269
  22. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_cavity_product line 293
  23. def OAI.SKFluctuations.Hierarchy.cavityEmbed line 334
  24. theorem OAI.SKFluctuations.Hierarchy.cavityEmbed_inl line 340
  25. theorem OAI.SKFluctuations.Hierarchy.cavityEmbed_inr line 343
  26. theorem OAI.SKFluctuations.Hierarchy.integral_zeroRowGaussian line 348
  27. theorem OAI.SKFluctuations.Hierarchy.shiftedContinuation_zeroRow line 368
  28. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_zeroRow line 378
  29. def OAI.SKFluctuations.Hierarchy.zeroRowSteps line 388
  30. theorem OAI.SKFluctuations.Hierarchy.zeroRowSteps_ordered line 392
  31. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_zeroRow line 400
  32. def OAI.SKFluctuations.Hierarchy.ReplicaTree.zeroRow line 414
  33. def OAI.SKFluctuations.Hierarchy.ReplicaTree.zeroRowAssignment line 422
  34. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.weight_zeroRow line 429
  35. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_zeroRow line 456
  36. theorem OAI.SKFluctuations.Hierarchy.spinPartition_spin_equiv line 478
  37. theorem OAI.SKFluctuations.Hierarchy.spinLogPartition_spin_equiv line 483
  38. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_spin_equiv line 491
  39. theorem OAI.SKFluctuations.Hierarchy.spinWeight_spin_equiv line 501
  40. def OAI.SKFluctuations.Hierarchy.ReplicaTree.spinEquiv line 510
  41. def OAI.SKFluctuations.Hierarchy.ReplicaTree.spinAssignmentEquiv line 516
  42. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.weight_spin_equiv line 524
  43. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_spin_equiv line 544