OAI/Probability/InvariantIsing/Fields/PriorReplicaAverage.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Observable and replica averages for the actual fixed-prior Gibbs measure.

  1. def OAI.InvariantIsing.priorNamespacedObservableAverage line 11
  2. lemma OAI.InvariantIsing.measurable_priorNamespacedObservableMean line 20
  3. lemma OAI.InvariantIsing.priorNamespacedObservableAverage_integrable line 37
  4. theorem OAI.InvariantIsing.priorFrozenGaussian_observableAverage line 57
  5. theorem OAI.InvariantIsing.priorFrozenDiagonal_observableAverage line 84
  6. def OAI.InvariantIsing.priorNamespacedReplicaAverage line 103
  7. lemma OAI.InvariantIsing.measurable_priorNamespacedReplicaMean line 113
  8. theorem OAI.InvariantIsing.priorFrozenGaussian_replicaAverage line 125