OAI/Probability/InvariantIsing/Cavity/CavityBoundedReweighting.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Bounded positive reweighting of random probability priors. Its replica-test limit follows from the unreweighted extra-replica limits.

  1. def OAI.InvariantIsing.cavityWeightNormalizer line 15
  2. def OAI.InvariantIsing.cavityWeightNumerator line 18
  3. def OAI.InvariantIsing.cavityWeightedReplicaMean line 22
  4. lemma OAI.InvariantIsing.measurable_cavityWeightNormalizer line 26
  5. lemma OAI.InvariantIsing.measurable_cavityWeightNumerator line 35
  6. lemma OAI.InvariantIsing.cavityWeightNormalizer_mem line 50
  7. lemma OAI.InvariantIsing.cavityWeightNumerator_abs_le line 64
  8. lemma OAI.InvariantIsing.cavityWeightNumerator_mul_normalizer line 83
  9. theorem OAI.InvariantIsing.cavity_bounded_reweighted_test_tendsto line 90
  10. theorem OAI.InvariantIsing.cavity_bounded_log_normalizer_tendsto line 144