SpectralDiagonalPerturbation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The deterministic spectral-diagonal perturbation as an exact eigenvalue shift.

def OAI.InvariantIsing.diagonalPerturbedEigenvalues line 15
theorem OAI.InvariantIsing.rotatedEnergy_diagonalPerturbation line 21
Source documentation
This is the first term of the manuscript's perturbation, including its coefficient N e_N, in the actual rotated Ising Hamiltonian.
```
theorem rotatedEnergy_diagonalPerturbation {N m : ℕ} (hN : 0 < N)
    (eig : Fin N → ℝ) (U : Rotation N) (I : Fin m → Finset (Fin N))
    (v : Fin m → ℝ) (t : ℝ) (σ : Spin N) :
    rotatedEnergy (diagonalPerturbedEigenvalues eig I v t) U σ =
      t * rotatedEnergy eig U σ + N * perturbationScale N * ∑ a, v a * projectedOverlap U (I a) σ σ := by
…
```
Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.rotatedEnergy, OAI.InvariantIsing.diagonalPerturbedEigenvalues, OAI.InvariantIsing.projectedOverlap
lemma OAI.InvariantIsing.diagonalPerturbedEigenvalues_abs_le line 60

lemma OAI.InvariantIsing.rotatedEnergy_diagonal_coordinate line 91

Source documentation

Replacing one diagonal coordinate adds exactly its bounded observable, even when all other spectral coordinates and the temperature are present.

lemma rotatedEnergy_diagonal_coordinate {N m : ℕ} (hN : 0 < N)
    (eig : Fin N → ℝ) (U : Rotation N) (I : Fin m → Finset (Fin N))
    (v : Fin m → ℝ) (t : ℝ) (a : Fin m) (w : ℝ) (σ : Spin N) :
    rotatedEnergy (diagonalPerturbedEigenvalues eig I (Function.update v a w) t) U σ =
      rotatedEnergy (diagonalPerturbedEigenvalues eig I (Function.update v a 0) t) U σ +
        N * perturbationScale N * w * projectedOverlap U (I a) σ σ := by
…

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

lemma OAI.InvariantIsing.abs_rotatedEnergy_diagonalPerturbation_le line 113