ReplicaContractions.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite replica contractions in the spectral Ward calculation

The sums over two spectral coordinate groups contract into products of projected overlaps. These are exact finite identities, with no symmetry or full-support requirement on the deterministic spin prior.

def OAI.InvariantIsing.gibbsPairAverage line 23
Source documentation
Independent replicas sampled from the same finite Gibbs law.
```
def gibbsPairAverage (w H : S → ℝ) (A : S → S → ℝ) : ℝ :=
…
```
def OAI.InvariantIsing.blockOverlap line 27
Source documentation
Unnormalized projected overlap; division by N is applied after contraction.
```
def blockOverlap (x : S → ι → ℝ) (I : Finset ι) (σ τ : S) : ℝ :=
…
```
lemma OAI.InvariantIsing.gibbsAverage_finset_sum line 30
lemma OAI.InvariantIsing.gibbsAverage_sub line 35
lemma OAI.InvariantIsing.gibbsPairAverage_finset_sum line 39
lemma OAI.InvariantIsing.gibbsAverage_mul_gibbsAverage line 49

lemma OAI.InvariantIsing.coordinate_fourth_contraction line 60

Source documentation

The direct Hamiltonian term contracts into a one-replica diagonal product.

lemma coordinate_fourth_contraction (w H : S → ℝ) (x : S → ι → ℝ) (I J : Finset ι) :
    (∑ i ∈ I, ∑ j ∈ J, gibbsAverage w H (fun σ => (x σ i * x σ j) ^ 2)) =
      gibbsAverage w H (fun σ => blockOverlap x I σ σ * blockOverlap x J σ σ) := by
…

Mentions: OAI.InvariantIsing.gibbsAverage, OAI.InvariantIsing.blockOverlap

lemma OAI.InvariantIsing.coordinate_mean_square_contraction line 74

Source documentation

The Gibbs-ratio subtraction contracts into a two-replica overlap product.

lemma coordinate_mean_square_contraction (w H : S → ℝ) (x : S → ι → ℝ) (I J : Finset ι) :
    (∑ i ∈ I, ∑ j ∈ J, gibbsAverage w H (fun σ => x σ i * x σ j) ^ 2) =
      gibbsPairAverage w H (fun σ τ => blockOverlap x I σ τ * blockOverlap x J σ τ) := by
…

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

lemma OAI.InvariantIsing.coordinate_difference_contraction line 89