OAI/Probability/InvariantIsing/Arrays/TensorWardReplica.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.referenceReplicaMean_finiteGibbs line 19
2. lemma OAI.InvariantIsing.referenceReplicaMean_one line 26
3. lemma OAI.InvariantIsing.referenceReplicaMean_two line 35
4. lemma OAI.InvariantIsing.referenceReplicaMean_three line 44
5. lemma OAI.InvariantIsing.finiteGibbsVariation_reference line 65
6. lemma OAI.InvariantIsing.finiteGibbsVariation_pair_reference line 83

   Source documentation

   A pair-state derivative reduces to two- and three-replica averages under the original state prior.

   lemma finiteGibbsVariation_pair_reference (ν : Measure S) [IsProbabilityMeasure ν]
       (H A : S → ℝ) (O dO : S → S → ℝ) :
       finiteGibbsVariation (fun p : S × S => ν.real {p.1} * ν.real {p.2})
         (fun p => H p.1 + H p.2) (fun p => O p.1 p.2)
         (fun p => A p.1 + A p.2) (fun p => dO p.1 p.2) =
         referenceReplicaMean ν H (fun σ : Fin 2 → S =>
           dO (σ 0) (σ 1) + O (σ 0) (σ 1) * (A (σ 0) + A (σ 1))) -
         2 * referenceReplicaMean ν H (fun σ : Fin 3 → S => O (σ 0) (σ 1) * A (σ 2)) := by
   …

   Mentions: OAI.InvariantIsing.finiteGibbsVariation

7. lemma OAI.InvariantIsing.gaussianWardCorrection_reference line 105
8. lemma OAI.InvariantIsing.gibbsKernelCorrection_reference line 118
9. lemma OAI.InvariantIsing.gibbsKernelCorrection_pair_reference line 133

   Source documentation

   Pair-state Gaussian corrections can be exhausted on the product prior without expanding them into six individually named replicas.

   lemma gibbsKernelCorrection_pair_reference (ν : Measure S) [IsProbabilityMeasure ν]
       (H : S × S → ℝ) (C : (S × S) → (S × S) → (S × S) → ℝ) :
       gibbsKernelCorrection (fun p : S × S => ν.real {p.1} * ν.real {p.2}) H C =
         referenceReplicaMean (ν.prod ν) H (fun σ : Fin 1 → S × S => C (σ 0) (σ 0) (σ 0)) -
         referenceReplicaMean (ν.prod ν) H (fun σ : Fin 2 → S × S => C (σ 0) (σ 0) (σ 1)) -
         referenceReplicaMean (ν.prod ν) H
           (fun σ : Fin 2 → S × S => C (σ 0) (σ 1) (σ 0) + C (σ 0) (σ 1) (σ 1)) +
         2 * referenceReplicaMean (ν.prod ν) H (fun σ : Fin 3 → S × S => C (σ 0) (σ 1) (σ 2)) := by
   …

   Mentions: OAI.InvariantIsing.gibbsKernelCorrection