OAI/Probability/InvariantIsing/Cavity/CavityHaarPenalizedLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual capped cavity logarithm with its geometric penalty has its deterministic-block limit after fresh-Haar averaging.

  1. theorem OAI.InvariantIsing.cavity_haar_penalized_coefficient_limit line 14