Model.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Finite-volume invariant Ising pressure

The spin prior is uniform probability, as in (1.1) and (7.1) of All-temperature pressure for orthogonally invariant Ising spin glasses. These deterministic comparison lemmas do not assume any asymptotic pressure formula.

abbrev OAI.InvariantIsing.Spin line 20
Source documentation
The cube, with exactly 2^N configurations.
Also declared: ComparatorChallenges/InvariantIsing.lean:14 (same declaration text).
```
abbrev Spin (N : ℕ) := Fin N → Bool
```
def OAI.InvariantIsing.spinValue line 23
Source documentation
Real spin coordinates.
Also declared: ComparatorChallenges/InvariantIsing.lean:16 (same declaration text).
```
def spinValue (b : Bool) : ℝ := if b then 1 else -1
```
lemma OAI.InvariantIsing.abs_spinValue line 25
lemma OAI.InvariantIsing.spinValue_sq line 28
def OAI.InvariantIsing.logPartition line 32
Source documentation
Log partition with the uniform probability prior on a finite state space.
Also declared: ComparatorChallenges/InvariantIsing.lean:18 (same declaration text).
```
def logPartition {X : Type*} [Fintype X] (H : X → ℝ) : ℝ :=
…
```
lemma OAI.InvariantIsing.sum_exp_pos line 35
lemma OAI.InvariantIsing.logPartition_eq line 39
lemma OAI.InvariantIsing.logPartition_add_const line 45
lemma OAI.InvariantIsing.logPartition_le_add line 54
lemma OAI.InvariantIsing.abs_logPartition_sub_le line 64
def OAI.InvariantIsing.quadraticEnergy line 76
Source documentation
Quadratic interaction energy, including the diagonal.
```
def quadraticEnergy {N : ℕ} (J : Matrix (Fin N) (Fin N) ℝ) (σ : Spin N) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.Spin
def OAI.InvariantIsing.fieldEnergy line 80
Source documentation
Deterministic magnetic energy.
Also declared: ComparatorChallenges/InvariantIsing.lean:21 (same declaration text).
```
def fieldEnergy {N : ℕ} (c : Fin N → ℝ) (σ : Spin N) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.Spin
def OAI.InvariantIsing.pressure line 84
Source documentation
Finite-volume pressure, normalized per site and by the probability spin prior.
```
def pressure {N : ℕ} (J : Matrix (Fin N) (Fin N) ℝ) (c : Fin N → ℝ) : ℝ :=
…
```
lemma OAI.InvariantIsing.fieldEnergy_sub line 87
lemma OAI.InvariantIsing.abs_fieldEnergy_sub_le line 91
lemma OAI.InvariantIsing.abs_pressure_sub_field_le line 100
Source documentation
Equation (7.26): the normalized pressure is Lipschitz in the average field distance.
```
lemma abs_pressure_sub_field_le {N : ℕ} (J : Matrix (Fin N) (Fin N) ℝ)
    (c d : Fin N → ℝ) :
    |pressure J c - pressure J d| ≤ (N : ℝ)⁻¹ * ∑ i, |c i - d i| := by
…
```
Mentions: OAI.InvariantIsing.pressure

lemma OAI.InvariantIsing.quadraticEnergy_add_scalar line 112

Source documentation

Scalar diagonal shifts are deterministic on the Ising cube.

lemma quadraticEnergy_add_scalar {N : ℕ} (J : Matrix (Fin N) (Fin N) ℝ)
    (a : ℝ) (σ : Spin N) :
    quadraticEnergy (J + a • (1 : Matrix (Fin N) (Fin N) ℝ)) σ =
      quadraticEnergy J σ + a * N / 2 := by
…

Mentions: OAI.InvariantIsing.Spin, OAI.InvariantIsing.quadraticEnergy

lemma OAI.InvariantIsing.pressure_add_scalar line 136

Source documentation

Equation (6.7): adding a scalar to the spectrum shifts pressure by half that scalar.

lemma pressure_add_scalar {N : ℕ} (hN : 0 < N)
    (J : Matrix (Fin N) (Fin N) ℝ) (c : Fin N → ℝ) (a : ℝ) :
    pressure (J + a • (1 : Matrix (Fin N) (Fin N) ℝ)) c = pressure J c + a / 2 := by
…

Mentions: OAI.InvariantIsing.pressure

lemma OAI.InvariantIsing.abs_pressure_sub_interaction_le line 150
Source documentation
A pointwise energy comparison gives the deterministic pressure comparison used for spectral approximation in Section 6.
```
lemma abs_pressure_sub_interaction_le {N : ℕ}
    (J K : Matrix (Fin N) (Fin N) ℝ) (c : Fin N → ℝ) (δ : ℝ)
    (h : ∀ σ : Spin N, |quadraticEnergy J σ - quadraticEnergy K σ| ≤ N * δ) :
    |pressure J c - pressure K c| ≤ (N : ℝ)⁻¹ * (N * δ) := by
…
```
Mentions: OAI.InvariantIsing.Spin, OAI.InvariantIsing.quadraticEnergy, OAI.InvariantIsing.pressure

lemma OAI.InvariantIsing.logPartition_bounds line 163

Source documentation

The elementary log-sum bound, with the probability prior's entropy cost.

lemma logPartition_bounds {X : Type*} [Fintype X] [Nonempty X]
    (H : X → ℝ) (M : ℝ) (hM : ∀ x, H x ≤ M) (hx : ∃ x, H x = M) :
    M - Real.log (Fintype.card X) ≤ logPartition H ∧ logPartition H ≤ M := by
…

Mentions: OAI.InvariantIsing.logPartition

lemma OAI.InvariantIsing.log_card_spin line 184
Source documentation
Uniform cube entropy is N log 2.
```
lemma log_card_spin (N : ℕ) : Real.log (Fintype.card (Spin N)) = N * Real.log 2 := by
…
```
Mentions: OAI.InvariantIsing.Spin

lemma OAI.InvariantIsing.finite_groundState_squeeze line 190

Source documentation

Soft maximum estimate used in the zero-temperature corollary, valid at every finite dimension and every positive inverse temperature.

lemma finite_groundState_squeeze {N : ℕ} (hN : 0 < N) (H : Spin N → ℝ)
    (β E : ℝ) (hβ : 0 < β) (hE : ∀ σ, H σ ≤ N * E)
    (hatt : ∃ σ, H σ = N * E) :
    E - Real.log 2 / β ≤ (N : ℝ)⁻¹ * logPartition (fun σ => β * H σ) / β ∧
      (N : ℝ)⁻¹ * logPartition (fun σ => β * H σ) / β ≤ E := by
…

Mentions: OAI.InvariantIsing.Spin, OAI.InvariantIsing.logPartition