OAI/Probability/InvariantIsing/Cavity/CavityExtraReplicaPrefix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Extra replicas are tested by restriction to the original prefix. This preserves the actual finite spectral observable when passing from numerator moments to normalized cavity-spin expectations.

  1. def OAI.InvariantIsing.cavityReplicaPrefixTest line 16
  2. lemma OAI.InvariantIsing.cavity_extra_replica_identity_fin line 23
  3. lemma OAI.InvariantIsing.cavityFiniteReplicaSpectralBlock_prefix line 50
  4. lemma OAI.InvariantIsing.cavityLabeledReplicaTest_prefix line 59
  5. lemma OAI.InvariantIsing.cavityLabeledCappedNumerator_mul_normalizer line 73