TensorFiniteWard.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Finite-prior Gaussian insertions in the spectral Haar Ward calculation. The covariance correction is derived by Gaussian integration by parts, with no assumed Ward identity. Finite spin/leaf restrictions are permitted to have zero prior weights.

def OAI.InvariantIsing.gaussianWardCorrection line 24
Source documentation
The exact correction obtained from inserting the derivative of a Gaussian Hamiltonian into a normalized finite Gibbs average. The kernel need not be symmetric: its first endpoint is the differentiated one.
```
def gaussianWardCorrection (w H O : S → ℝ) (K : S → S → ℝ) : ℝ :=
…
```

lemma OAI.InvariantIsing.gaussian_replica_selected_insertion line 32

Source documentation

Insertion in any specified replica, with an arbitrary bounded finite replica test. No symmetry or constant-diagonal assumption is used.

lemma gaussian_replica_selected_insertion {d r : ℕ} {w : S → ℝ}
    (hw : GibbsReference w) (H : S → ℝ) (A C : S → Fin (d + 1) → ℝ)
    (l : Fin r) (D : (Fin r → S) → ℝ) :
    (∫ g, ∑ σ : Fin r → S,
      D σ * (linearGaussian A g (σ l) * replicaGibbs w H C g σ)
        ∂Measure.pi (fun _ : Fin (d + 1) => gaussianReal 0 1)) =
      ∫ g, ∑ σ : Fin r → S, D σ * (replicaGibbs w H C g σ *
        ∑ k, (gaussianCross A C (σ l) (σ k) -
          ∑ z, gaussianGibbs w H C g z * gaussianCross A C (σ l) z))
        ∂Measure.pi (fun _ : Fin (d + 1) => gaussianReal 0 1) := by
…

lemma OAI.InvariantIsing.integrable_gaussian_gibbs_linear_test line 50
lemma OAI.InvariantIsing.integrable_gaussian_gibbs_linear_product line 63
lemma OAI.InvariantIsing.integrable_gaussian_gibbs_test line 79

lemma OAI.InvariantIsing.gaussian_gibbs_test_insertion line 95

Source documentation

The Gibbs insertion in the current replica produces the derivative covariance with one subtraction replica.

lemma gaussian_gibbs_test_insertion {d : ℕ} {w : S → ℝ}
    (hw : GibbsReference w) (H O : S → ℝ) (A C : S → Fin (d + 1) → ℝ) :
    (∫ g, gibbsAverage w (fun x => H x + linearGaussian C g x)
      (fun x => O x * linearGaussian A g x)
      ∂Measure.pi (fun _ : Fin (d + 1) => gaussianReal 0 1)) =
      ∫ g, gibbsAverage w (fun x => H x + linearGaussian C g x)
        (fun x => O x * gaussianCross A C x x) -
        gibbsPairAverage w (fun x => H x + linearGaussian C g x)
          (fun x y => O x * gaussianCross A C x y)
        ∂Measure.pi (fun _ : Fin (d + 1) => gaussianReal 0 1) := by
…

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

lemma OAI.InvariantIsing.gaussian_gibbs_normalization_insertion line 142
lemma OAI.InvariantIsing.integrable_gaussian_pair_test line 215
lemma OAI.InvariantIsing.integrable_gaussian_triple_test line 240

theorem OAI.InvariantIsing.gaussian_gibbs_covariance_insertion line 275

Source documentation

Exact Gaussian covariance-derivative correction for a finite prior. The first coefficient map is the Hamiltonian derivative and the second is the Gaussian coefficient in the Gibbs exponent.

theorem gaussian_gibbs_covariance_insertion {d : ℕ} {w : S → ℝ}
    (hw : GibbsReference w) (H O : S → ℝ) (A C : S → Fin (d + 1) → ℝ) :
    (∫ g, gibbsAverage w (fun x => H x + linearGaussian C g x)
        (fun x => O x * linearGaussian A g x) -
      gibbsAverage w (fun x => H x + linearGaussian C g x) O *
        gibbsAverage w (fun x => H x + linearGaussian C g x) (linearGaussian A g)
      ∂Measure.pi (fun _ : Fin (d + 1) => gaussianReal 0 1)) =
      ∫ g, gaussianWardCorrection w (fun x => H x + linearGaussian C g x) O
        (gaussianCross A C)
        ∂Measure.pi (fun _ : Fin (d + 1) => gaussianReal 0 1) := by
…

Mentions: OAI.InvariantIsing.gibbsAverage, OAI.InvariantIsing.gaussianWardCorrection