OAI/Probability/InvariantIsing/Arrays/TensorCascadeReplicaAverage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual enriched replica average is a cascade mixture of fixed-prior spin/leaf averages. The common rotation is retained in the mixture.

  1. lemma OAI.InvariantIsing.referenceReplicaMean_gibbsProbability line 16
  2. lemma OAI.InvariantIsing.tensorCascadeDisorderShuffle_preserving line 24
  3. lemma OAI.InvariantIsing.tensorRestrictionHamiltonian_id_eq line 38
  4. theorem OAI.InvariantIsing.tensorNamespacedReplicaAverage_cascade_mixture line 46