OAI/Probability/InvariantIsing/Spectral/SpectralEndpoints.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Endpoint regularity for the finite spectral-group functions.

  1. theorem OAI.InvariantIsing.projectedResolventDerivative_eq_regular line 18
  2. theorem OAI.InvariantIsing.continuousWithinAt_projectedResolventDerivative_zero line 51
  3. theorem OAI.InvariantIsing.continuousAt_projectedResolventDerivative_pos line 70
  4. theorem OAI.InvariantIsing.continuousOn_projectedResolventDerivative line 87
  5. theorem OAI.InvariantIsing.projectedResolventDerivative_constant line 97
  6. theorem OAI.InvariantIsing.projectedResolvent_eq_regular line 106
  7. theorem OAI.InvariantIsing.hasDerivWithinAt_projectedResolvent_zero line 125

    Source documentation

    The right derivative at the origin is the spectral mass, as asserted in manuscript rot:f-derivative.

    theorem hasDerivWithinAt_projectedResolvent_zero (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
    (hρsum : ∑ a, ρ a = 1) (a : ι) :
    HasDerivWithinAt (projectedResolvent ρ eig hρ hρsum a) (ρ a) (Ioi 0) 0 := by
…

    Mentions: OAI.InvariantIsing.projectedResolvent