SpectralExistence.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The inverse Cauchy transform of a finite alphabet always lies strictly above its largest atom. This supplies existence, as well as uniqueness, for the resolvent used by the finite-alphabet cavity construction.

theorem OAI.InvariantIsing.continuousOn_finiteResolvent line 21

theorem OAI.InvariantIsing.exists_unique_finiteResolvent_solution line 31

Source documentation

Existence and uniqueness above an upper edge carrying positive mass.

theorem exists_unique_finiteResolvent_solution {ρ eig : ι → ℝ} {a₀ : ι} {x : ℝ}
    (hρ : ∀ a, 0 ≤ ρ a) (hρsum : ∑ a, ρ a = 1)
    (ha₀ : 0 < ρ a₀) (he : ∀ a, eig a ≤ eig a₀) (hx : 0 < x) :
    ∃! b : ℝ, (∀ a, eig a < b) ∧ finiteResolvent ρ eig b = x := by
…

Mentions: OAI.InvariantIsing.finiteResolvent

theorem OAI.InvariantIsing.exists_unique_finiteResolvent_of_pos line 69
Source documentation
In particular every finite spectral probability law with positive masses has an uncapped inverse at every positive argument.
```
theorem exists_unique_finiteResolvent_of_pos {ρ eig : ι → ℝ} {x : ℝ}
    (hρ : ∀ a, 0 < ρ a) (hρsum : ∑ a, ρ a = 1) (hx : 0 < x) :
    ∃! b : ℝ, (∀ a, eig a < b) ∧ finiteResolvent ρ eig b = x := by
…
```
Mentions: OAI.InvariantIsing.finiteResolvent