OAI/Probability/InvariantIsing/Cavity/CavityCappedBlockLog.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Replacement of random cavity blocks inside the capped expected logarithm. The hypotheses are the proved coefficient and prior bounds.

  1. theorem OAI.InvariantIsing.cavity_capped_block_log_limit line 15