OAI/Probability/InvariantIsing/Spectral/FiniteSpectralContinuity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Continuity under changes of the positive masses of a fixed finite spectral alphabet. The inverse is compared using its defining resolvent equation.

  1. theorem OAI.InvariantIsing.finiteResolvent_tendsto_weights line 16
  2. theorem OAI.InvariantIsing.finiteInverse_tendsto_weights line 22
  3. theorem OAI.InvariantIsing.finiteR_tendsto_weights_pos line 69
  4. theorem OAI.InvariantIsing.finiteR_tendsto_weights_zero line 89
  5. theorem OAI.InvariantIsing.finiteR_tendsto_weights_nonneg line 128
  6. theorem OAI.InvariantIsing.finiteR_uniform_weights line 141

    Source documentation

    Uniformity on the whole interval includes the transform's value at zero.

    theorem finiteR_uniform_weights (ρs : ℕ → ι → ℝ) (ρ eig : ι → ℝ)
    (hspos : ∀ k a, 0 < ρs k a) (hssum : ∀ k, ∑ a, ρs k a = 1)
    (hpos : ∀ a, 0 < ρ a) (hsum : ∑ a, ρ a = 1)
    (hρs : Tendsto ρs atTop (𝓝 ρ)) :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ k in atTop, ∀ x ∈ Icc (0 : ℝ) 1,
      |finiteR (ρs k) eig (hspos k) (hssum k) x - finiteR ρ eig hpos hsum x| < ε := by
…

    Mentions: OAI.InvariantIsing.finiteR

  7. theorem OAI.InvariantIsing.finiteVariational_tendsto_weights line 173