Rotation.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Ising pressure on an orthogonal spectral orbit

The interaction is defined using a real linear isometry, so orthogonality is part of its type. The bounds hold pointwise in the rotation; no Haar or independence assumption is needed for these finite-volume estimates.

abbrev OAI.InvariantIsing.Rotation line 20
Also declared: ComparatorChallenges/InvariantIsing.lean:24 (same declaration text).
def OAI.InvariantIsing.spinVector line 23
Also declared: ComparatorChallenges/InvariantIsing.lean:29 (same declaration text).
lemma OAI.InvariantIsing.spinVector_apply line 26
lemma OAI.InvariantIsing.spinVector_norm_sq line 29
lemma OAI.InvariantIsing.rotated_spin_sq_sum line 34
def OAI.InvariantIsing.rotatedEnergy line 40
Source documentation
The quadratic energy in spectral coordinates, equal to σᵀ Uᵀ diag(eig) U σ / 2.
Also declared: ComparatorChallenges/InvariantIsing.lean:32 (same declaration text).
```
def rotatedEnergy {N : ℕ} (eig : Fin N → ℝ) (U : Rotation N) (σ : Spin N) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin
def OAI.InvariantIsing.rotatedPressure line 44
Source documentation
Equation (1.1), with an optional deterministic magnetic field.
Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:35 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.rotatedPressure@path.
```
def rotatedPressure {N : ℕ} (eig : Fin N → ℝ) (U : Rotation N)
    (c : Fin N → ℝ) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.Rotation
lemma OAI.InvariantIsing.rotatedEnergy_constant line 48
lemma OAI.InvariantIsing.logPartition_zero line 53
lemma OAI.InvariantIsing.rotatedPressure_constant line 58

lemma OAI.InvariantIsing.abs_rotatedEnergy_sub_le line 69

Source documentation

Pointwise operator comparison in spectral coordinates.

lemma abs_rotatedEnergy_sub_le {N : ℕ} (eig κ : Fin N → ℝ) (U : Rotation N)
    (δ : ℝ) (hδ : ∀ i, |eig i - κ i| ≤ δ) (σ : Spin N) :
    |rotatedEnergy eig U σ - rotatedEnergy κ U σ| ≤ δ * N / 2 := by
…

Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.rotatedEnergy

lemma OAI.InvariantIsing.abs_rotatedPressure_sub_le line 88

Source documentation

Equation (6.6), pointwise in the rotation and independent of the field.

lemma abs_rotatedPressure_sub_le {N : ℕ} (hN : 0 < N)
    (eig κ : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
    (δ : ℝ) (hδ : ∀ i, |eig i - κ i| ≤ δ) :
    |rotatedPressure eig U c - rotatedPressure κ U c| ≤ δ / 2 := by
…

Mentions: OAI.InvariantIsing.Rotation

lemma OAI.InvariantIsing.tendsto_pressure_scalar_spectrum line 109

Source documentation

The point-mass spectral specialization: spectra uniformly approaching a scalar have limiting pressure a/2 for every choice of rotations.

lemma tendsto_pressure_scalar_spectrum
    (eig : (N : ℕ) → Fin (N + 1) → ℝ) (U : (N : ℕ) → Rotation (N + 1))
    (a : ℝ) (δ : ℕ → ℝ) (hδ : Tendsto δ atTop (nhds 0))
    (heig : ∀ N i, |eig N i - a| ≤ δ N) :
    Tendsto (fun N => rotatedPressure (eig N) (U N) (fun _ => 0)) atTop (nhds (a / 2)) := by
…

Mentions: OAI.InvariantIsing.Rotation