OAI/Probability/InvariantIsing/Fields/SpinFactorization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact factorization of the Ising reference at zero interaction.

  1. lemma OAI.InvariantIsing.sum_exp_fieldEnergy line 13
  2. theorem OAI.InvariantIsing.logPartition_fieldEnergy line 24

    Source documentation

    The site factorization used before the backward Gaussian cascade recursion.

    theorem logPartition_fieldEnergy {N : ℕ} (c : Fin N → ℝ) :
    logPartition (fieldEnergy c) = ∑ i, Real.log (Real.cosh (c i)) := by
…

    Mentions: OAI.InvariantIsing.logPartition, OAI.InvariantIsing.fieldEnergy

  3. theorem OAI.InvariantIsing.noninteractingPressure_eq_logCosh line 33