OAI/Probability/InvariantIsing/Cavity/CavityRegularizedReweighting.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Extra-replica limits for bounded nonnegative factors, with the normalizer regularized before any cutoff is removed.

  1. def OAI.InvariantIsing.cavityRegularizedReplicaMean line 15
  2. theorem OAI.InvariantIsing.cavity_regularized_reweighted_test_tendsto line 19
  3. theorem OAI.InvariantIsing.cavity_floored_log_normalizer_tendsto line 73