OAI/Probability/InvariantIsing/Magnetic/RestrictedFiniteLogEvaluation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual finite spectral cavity logarithmic normalizer is exactly its variational trial value. All covariance and precision requirements are derived from the finite spectrum and its block geometry.

  1. theorem OAI.InvariantIsing.restricted_cavity_finite_log_evaluation line 19