OAI/Probability/InvariantIsing/Arrays/CountableWardMixture.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform fixed-prior Ward bounds survive a measurable mixture of countable reference measures.

  1. lemma OAI.InvariantIsing.measurable_mixtureReplicaMean line 14
  2. lemma OAI.InvariantIsing.measurable_integral_mixtureReplicaMean line 29
  3. lemma OAI.InvariantIsing.integrable_mixtureReplicaMean line 40
  4. theorem OAI.InvariantIsing.expectedReplicaWard_mixture_abs_le line 59