OAI/Probability/InvariantIsing/Cavity/CavityReplicaLinearity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite linear combinations of bounded replica tests commute with the normalized Gibbs average, including a zero denominator.

  1. lemma OAI.InvariantIsing.cavity_referenceReplicaMean_sum line 14
  2. lemma OAI.InvariantIsing.cavity_nested_replica_sum line 35