OAI/Probability/InvariantIsing/Cavity/CavityFieldModulus.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform plateau control for the actual strict finite cavity fields. The spectral derivative bound and the conditional-variance estimate turn convergence of overlap levels into asymptotic preservation of ties.

  1. lemma OAI.InvariantIsing.cavityFieldPrimitive_dist_le line 18
  2. lemma OAI.InvariantIsing.cavityStrictUniformField_height_le line 33
  3. lemma OAI.InvariantIsing.cavityStrictUniformField_magnetization_dist_le line 47
  4. theorem OAI.InvariantIsing.cavity_strict_field_asymptotic_ties line 63
  5. theorem OAI.InvariantIsing.cavity_strict_field_self_consistency line 94