SpectralContinuity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A quantitative estimate at zero for the finite spectral transform.

theorem OAI.InvariantIsing.finiteR_sub_mean line 17

Source documentation

An exact remainder identity for the finite inverse resolvent.

theorem finiteR_sub_mean (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
    (hρsum : ∑ a, ρ a = 1) {x : ℝ} (hx : 0 < x) :
    finiteR ρ eig hρ hρsum x - ∑ a, ρ a * eig a =
      ∑ a, ρ a * (finiteR ρ eig hρ hρsum x - eig a) ^ 2 /
        (finiteInverse ρ eig hρ hρsum x - eig a) := by
…

Mentions: OAI.InvariantIsing.finiteR, OAI.InvariantIsing.finiteInverse

theorem OAI.InvariantIsing.mean_le_finiteR line 44

theorem OAI.InvariantIsing.finiteR_sub_mean_le line 54

Source documentation

The uniform O(K²x) estimate from manuscript gen:R-at-zero.

theorem finiteR_sub_mean_le (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
    (hρsum : ∑ a, ρ a = 1) {K x : ℝ} (_hK : 0 ≤ K)
    (heig : ∀ a, |eig a| ≤ K) (hx : 0 < x) (hsmall : 4 * K * x ≤ 1) :
    finiteR ρ eig hρ hρsum x - ∑ a, ρ a * eig a ≤ 8 * K ^ 2 * x := by
…

Mentions: OAI.InvariantIsing.finiteR

theorem OAI.InvariantIsing.continuousAt_finiteR_zero line 96