OAI/Probability/InvariantIsing/Core/PairGibbs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.GibbsReference_pair line 17
2. lemma OAI.InvariantIsing.finitePartition_pair line 23
3. lemma OAI.InvariantIsing.finiteGibbs_pair line 33
4. lemma OAI.InvariantIsing.gibbsAverage_pair line 39
5. lemma OAI.InvariantIsing.gibbsPairAverage_add line 44
6. lemma OAI.InvariantIsing.gibbsPairAverage_fst line 49
7. lemma OAI.InvariantIsing.gibbsPairAverage_swap line 61
8. lemma OAI.InvariantIsing.gibbsPairAverage_snd line 71
9. lemma OAI.InvariantIsing.gibbsAverage_pair_sum line 76
10. lemma OAI.InvariantIsing.hasDerivAt_gibbsPairAverage line 85

    Source documentation

    The two-replica derivative has one Hamiltonian insertion in each existing replica and two Gibbs normalization subtractions.

    lemma hasDerivAt_gibbsPairAverage {w : S → ℝ} (hw : GibbsReference w)
        {H : ℝ → S → ℝ} {A : ℝ → S → S → ℝ}
        {dH : S → ℝ} {dA : S → S → ℝ} {t : ℝ}
        (hH : ∀ σ, HasDerivAt (fun s => H s σ) (dH σ) t)
        (hA : ∀ σ τ, HasDerivAt (fun s => A s σ τ) (dA σ τ) t) :
        HasDerivAt (fun s => gibbsPairAverage w (H s) (A s))
          (gibbsPairAverage w (H t) dA +
            gibbsPairAverage w (H t) (fun σ τ => A t σ τ * (dH σ + dH τ)) -
            2 * gibbsPairAverage w (H t) (A t) * gibbsAverage w (H t) dH) t := by
    …

    Mentions: OAI.InvariantIsing.gibbsPairAverage, OAI.InvariantIsing.gibbsAverage