OAI/Probability/InvariantIsing/Cavity/CavityMovingMoments.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Matching replica moments compare two varying models directly. This applies to the physical system and a refining finite cascade without postulating a limiting random probability measure for either model.

  1. theorem OAI.InvariantIsing.cavity_moving_weighted_moments line 15
  2. theorem OAI.InvariantIsing.cavity_moving_floored_log line 63