SpectralGroupIdentification.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A canonical group quantile and its diagonal are identified by the spectral symbols and roots derived from the actual Ward equations.

theorem OAI.InvariantIsing.spectralGroup_identification_of_symbol_root line 21

Source documentation

Equality with the reconstructed spectral group follows from its proved symbol and root formulas and the AE path uniqueness theorem.

theorem spectralGroup_identification_of_symbol_root (ρ eig : ι → ℝ)
    (hρ : ∀ a, 0 < ρ a) (hρsum : ∑ a, ρ a = 1) (p q : OverlapPath) (d : ℝ) (a : ι)
    (hsymbol : ∀ᵐ s ∂pathMeasure, pathSymbol d q.val s =
      projectedResolvent ρ eig hρ hρsum a (deficit p (p s)))
    (hroot : Function.rightLim q.val 0 = Function.rightLim p.val 0 *
      projectedResolventDerivative ρ eig hρ hρsum a (deficit p (Function.rightLim p.val 0))) :
    d = spectralGroupDiagonal ρ eig hρ hρsum p a ∧
      q.val =ᵐ[pathMeasure] spectralGroupPath ρ eig hρ hρsum p a := by
…

Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.pathSymbol, OAI.InvariantIsing.projectedResolvent, OAI.InvariantIsing.projectedResolventDerivative, OAI.InvariantIsing.spectralGroupDiagonal, OAI.InvariantIsing.spectralGroupPath

theorem OAI.InvariantIsing.spectralGroups_identification_of_symbols_roots line 54

Source documentation

The finite family form keeps all group quantiles on one common full measure set, as needed for the actual limiting spectral-array law.

theorem spectralGroups_identification_of_symbols_roots (ρ eig : ι → ℝ)
    (hρ : ∀ a, 0 < ρ a) (hρsum : ∑ a, ρ a = 1) (p : OverlapPath)
    (q : ι → OverlapPath) (d : ι → ℝ)
    (hsymbol : ∀ a, ∀ᵐ s ∂pathMeasure, pathSymbol (d a) (q a).val s =
      projectedResolvent ρ eig hρ hρsum a (deficit p (p s)))
    (hroot : ∀ a, Function.rightLim (q a).val 0 = Function.rightLim p.val 0 *
      projectedResolventDerivative ρ eig hρ hρsum a (deficit p (Function.rightLim p.val 0))) :
    (∀ a, d a = spectralGroupDiagonal ρ eig hρ hρsum p a) ∧
      ∀ᵐ s ∂pathMeasure, ∀ a, q a s = spectralGroupPath ρ eig hρ hρsum p a s := by
…