OAI/Probability/InvariantIsing/Fields/PriorDiagonalStatistics.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The diagonal observable's actual CGF inherits concentration from both neighboring finite-prior log partition functions.

  1. def OAI.InvariantIsing.priorDiagonalCGF line 13
  2. theorem OAI.InvariantIsing.priorDiagonalCGF_statistics line 22