Spectral.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Finite spectral resolvents

The finite-alphabet arguments in Sections 3 and 5 of the manuscript use the unique solution of ∑ a, ρ a / (b - eig a) = x above all eigenvalues. The solution is unique and satisfies deterministic bounds. The weights may vanish; their sum being one is the only normalization.

def OAI.InvariantIsing.finiteResolvent line 24
Source documentation
The Cauchy transform of a finite spectral probability law.
```
def finiteResolvent (ρ eig : ι → ℝ) (b : ℝ) : ℝ :=
…
```
def OAI.InvariantIsing.finiteSecondResolvent line 28
Source documentation
The second resolvent moment, which controls the derivative of the inverse.
```
def finiteSecondResolvent (ρ eig : ι → ℝ) (b : ℝ) : ℝ :=
…
```
theorem OAI.InvariantIsing.exists_pos_spectral_weight line 31
theorem OAI.InvariantIsing.finiteResolvent_pos line 40
theorem OAI.InvariantIsing.finiteResolvent_strictAnti line 49

theorem OAI.InvariantIsing.finiteResolvent_solution_unique line 61

Source documentation

The finite-alphabet inverse is unique on its required branch.

theorem finiteResolvent_solution_unique {ρ eig : ι → ℝ} {b c x : ℝ}
    (hρ : ∀ a, 0 ≤ ρ a) (hρsum : ∑ a, ρ a = 1)
    (hb : ∀ a, eig a < b) (hc : ∀ a, eig a < c)
    (hbx : finiteResolvent ρ eig b = x) (hcx : finiteResolvent ρ eig c = x) :
    b = c := by
…

Mentions: OAI.InvariantIsing.finiteResolvent

theorem OAI.InvariantIsing.finiteResolvent_le line 73
theorem OAI.InvariantIsing.le_finiteResolvent line 84

theorem OAI.InvariantIsing.finiteR_bounds line 96

Source documentation

Section 6's bound for the uncapped inverse transform.

theorem finiteR_bounds {ρ eig : ι → ℝ} {b x l u : ℝ}
    (hρ : ∀ a, 0 ≤ ρ a) (hρsum : ∑ a, ρ a = 1)
    (hl : ∀ a, l ≤ eig a) (hu : ∀ a, eig a ≤ u)
    (hb : u < b) (hx : 0 < x) (hbx : finiteResolvent ρ eig b = x) :
    l ≤ b - 1 / x ∧ b - 1 / x ≤ u := by
…

Mentions: OAI.InvariantIsing.finiteResolvent

theorem OAI.InvariantIsing.finiteResolvent_translate line 118
theorem OAI.InvariantIsing.finiteResolvent_constant line 127
Source documentation
The transform of a point mass is the constant equal to its atom.
```
theorem finiteResolvent_constant {ρ : ι → ℝ} (hρsum : ∑ a, ρ a = 1)
    (b c : ℝ) :
    finiteResolvent ρ (fun _ => c) b = 1 / (b - c) := by
…
```
Mentions: OAI.InvariantIsing.finiteResolvent
theorem OAI.InvariantIsing.constant_spectrum_solution line 133
theorem OAI.InvariantIsing.finiteResolvent_sq_le_second line 141