OAI/Probability/InvariantIsing/Spectral/SpectralOrder.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Order and uniform perturbation bounds for finite spectral transforms.

  1. theorem OAI.InvariantIsing.finiteResolvent_mono_eig line 15
  2. theorem OAI.InvariantIsing.finiteInverse_mono_eig line 22
  3. theorem OAI.InvariantIsing.finiteR_mono_eig line 35
  4. theorem OAI.InvariantIsing.finiteR_perturbation line 45

    Source documentation

    Uniform coordinate perturbations give the same uniform error in R.

    theorem finiteR_perturbation (ρ eig eig' : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
    (hρsum : ∑ a, ρ a = 1) {δ : ℝ} (heig : ∀ a, |eig a - eig' a| ≤ δ)
    {x : ℝ} (hx : 0 ≤ x) :
    |finiteR ρ eig hρ hρsum x - finiteR ρ eig' hρ hρsum x| ≤ δ := by
…

    Mentions: OAI.InvariantIsing.finiteR