SpectralCalculus.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Differentiation of the finite spectral inverse. The inverse function theorem is applied to the already constructed inverse; no regularity of that inverse is assumed.

def OAI.InvariantIsing.finiteThirdResolvent line 25
Source documentation
Third resolvent moment.
```
def finiteThirdResolvent (ρ eig : ι → ℝ) (b : ℝ) : ℝ :=
…
```
theorem OAI.InvariantIsing.finiteSecondResolvent_pos line 28
theorem OAI.InvariantIsing.finiteSecondResolvent_sq_le_first_mul_third line 38
Source documentation
The Cauchy–Schwarz inequality used for convexity of x ↦ x R(t x).
```
theorem finiteSecondResolvent_sq_le_first_mul_third {ρ eig : ι → ℝ} {b : ℝ}
    (hρ : ∀ a, 0 ≤ ρ a) (hb : ∀ a, eig a < b) :
    finiteSecondResolvent ρ eig b ^ 2 ≤
      finiteResolvent ρ eig b * finiteThirdResolvent ρ eig b := by
…
```
Mentions: OAI.InvariantIsing.finiteSecondResolvent, OAI.InvariantIsing.finiteResolvent, OAI.InvariantIsing.finiteThirdResolvent
theorem OAI.InvariantIsing.hasStrictDerivAt_finiteResolvent line 51
theorem OAI.InvariantIsing.hasStrictDerivAt_finiteSecondResolvent line 63
def OAI.InvariantIsing.finiteInverse line 81
Source documentation
Inverse transform for a finite alphabet with positive masses. The value outside positive arguments is irrelevant to the application.
```
def finiteInverse (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
    (hρsum : ∑ a, ρ a = 1) (x : ℝ) : ℝ :=
…
```
theorem OAI.InvariantIsing.finiteInverse_spec line 85
theorem OAI.InvariantIsing.finiteInverse_left line 92

theorem OAI.InvariantIsing.hasStrictDerivAt_finiteInverse line 100

Source documentation

The exact inverse derivative appearing in the finite-spectrum calculation.

theorem hasStrictDerivAt_finiteInverse (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
    (hρsum : ∑ a, ρ a = 1) {x : ℝ} (hx : 0 < x) :
    HasStrictDerivAt (finiteInverse ρ eig hρ hρsum)
      (-1 / finiteSecondResolvent ρ eig (finiteInverse ρ eig hρ hρsum x)) x := by
…

Mentions: OAI.InvariantIsing.finiteInverse, OAI.InvariantIsing.finiteSecondResolvent

def OAI.InvariantIsing.finiteR line 121
Source documentation
Finite-alphabet R-transform, with its prescribed value at zero.
```
def finiteR (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
    (hρsum : ∑ a, ρ a = 1) (x : ℝ) : ℝ :=
…
```
theorem OAI.InvariantIsing.hasStrictDerivAt_finiteR line 125
theorem OAI.InvariantIsing.finiteR_derivative_nonneg line 141
theorem OAI.InvariantIsing.hasStrictDerivAt_finiteInverseDerivative line 152
def OAI.InvariantIsing.finiteEnergyDerivative line 169
Source documentation
First derivative of x R(x), in a form without cancellation at zero.
```
def finiteEnergyDerivative (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
    (hρsum : ∑ a, ρ a = 1) (x : ℝ) : ℝ :=
…
```
theorem OAI.InvariantIsing.hasStrictDerivAt_mul_finiteR line 174

theorem OAI.InvariantIsing.hasStrictDerivAt_finiteEnergyDerivative line 188

Source documentation

The second derivative used in manuscript up:energy.

theorem hasStrictDerivAt_finiteEnergyDerivative (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
    (hρsum : ∑ a, ρ a = 1) {x : ℝ} (hx : 0 < x) :
    HasStrictDerivAt (finiteEnergyDerivative ρ eig hρ hρsum)
      (2 * (x * finiteThirdResolvent ρ eig (finiteInverse ρ eig hρ hρsum x) -
        finiteSecondResolvent ρ eig (finiteInverse ρ eig hρ hρsum x) ^ 2) /
        finiteSecondResolvent ρ eig (finiteInverse ρ eig hρ hρsum x) ^ 3) x := by
…

Mentions: OAI.InvariantIsing.finiteEnergyDerivative, OAI.InvariantIsing.finiteThirdResolvent, OAI.InvariantIsing.finiteInverse, OAI.InvariantIsing.finiteSecondResolvent

theorem OAI.InvariantIsing.finiteEnergy_secondDerivative_nonneg line 204