OAI/Probability/InvariantIsing/Cavity/CavityPreliminaryLower.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One-sided removal of the logarithmic cap. Only the limiting finite model needs full moments; the finite physical increment is bounded below by each of its capped approximations.

  1. lemma OAI.InvariantIsing.cavity_preliminary_lower_of_caps line 16
  2. theorem OAI.InvariantIsing.cavity_finite_preliminary_lower line 37