OAI/Probability/InvariantIsing/Cavity/CavityMovingRatio.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Matching weighted moments determine unregularized bounded replica tests. The uniform negative-log second moment controls small random normalizers.

  1. theorem OAI.InvariantIsing.cavity_moving_unregularized_ratio line 15
  2. theorem OAI.InvariantIsing.cavity_moving_ratio_of_moments line 57