`OAI/Probability/InvariantIsing/Cavity/CavityPenaltyRate.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The extension penalty is negligible in each fixed-size cavity step.

lemma OAI.InvariantIsing.cavity_extension_penalty_tendsto line 14
lemma OAI.InvariantIsing.cavity_total_minimum_penalty_tendsto line 27