SpectralReconstruction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Algebraic reconstruction of spectral-group symbols and roots, as used in manuscript Proposition rot:paths, from the Ward equations.

theorem OAI.InvariantIsing.spectral_symbol_reconstruction line 18

Source documentation

The nonnegative solution of the finite spectral Ward equations is the projected inverse resolvent.

theorem spectral_symbol_reconstruction (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
    (hρsum : ∑ a, ρ a = 1) (α : ι → ℝ) (hα : ∀ a, 0 ≤ α a)
    (hward : ∀ a b, ρ b * α a - ρ a * α b =
      (eig a - eig b) * α a * α b) (a : ι) :
    α a = projectedResolvent ρ eig hρ hρsum a (∑ b, α b) := by
…

Mentions: OAI.InvariantIsing.projectedResolvent

theorem OAI.InvariantIsing.spectral_root_reconstruction line 72

Source documentation

The root Ward equations determine the normalized derivative weights. This also includes the zero-symbol endpoint and tied eigenvalues.

 theorem spectral_root_reconstruction (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
     (hρsum : ∑ a, ρ a = 1) {x : ℝ} (hx : 0 ≤ x) (r : ι → ℝ)
     (hward : ∀ a b, ρ b * r a - ρ a * r b =
       (eig a - eig b) *
         (projectedResolvent ρ eig hρ hρsum a x * r b +
          r a * projectedResolvent ρ eig hρ hρsum b x)) (a : ι) :
     r a = (∑ b, r b) * projectedResolventDerivative ρ eig hρ hρsum a x := by
…

Mentions: OAI.InvariantIsing.projectedResolvent, OAI.InvariantIsing.projectedResolventDerivative