OAI/Probability/InvariantIsing/Cavity/CavityLabeledModelNumerator.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Measurability and the literal product-prior formula for the finite cavity numerator used in extra-replica normalization.

  1. def OAI.InvariantIsing.cavityLabeledReplicaTest line 14
  2. lemma OAI.InvariantIsing.measurable_cavityLabeledReplicaTest line 20
  3. def OAI.InvariantIsing.cavityLabeledCappedNumerator line 32
  4. lemma OAI.InvariantIsing.measurable_cavityLabeledCappedNumerator line 41
  5. lemma OAI.InvariantIsing.cavityLabeledCappedNumerator_bound line 52
  6. lemma OAI.InvariantIsing.cavityLabeledCappedNumerator_eq line 65
  7. lemma OAI.InvariantIsing.integral_cavityLabeledCappedNumerator line 81