CanonicalRootReconstruction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Root reconstruction for a finite family of canonical overlap paths. The Ward equations and reconstructed symbols determine the roots, whose sum follows from the almost-everywhere path sum.

lemma OAI.InvariantIsing.projectedResolvent_deficit_path_root_tendsto line 20
lemma OAI.InvariantIsing.canonical_symbol_root_eq line 34
lemma OAI.InvariantIsing.canonical_group_roots_sum line 53

theorem OAI.InvariantIsing.canonical_group_root_reconstruction line 68

Source documentation

The actual root Ward equations fix every canonical group root once the symbols and the total path have been identified.

theorem canonical_group_root_reconstruction (ρ 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)))
    (hsum : ∀ᵐ s ∂pathMeasure, ∑ a, q a s = p s)
    (hward : ∀ a b, ρ b * Function.rightLim (q a).val 0 -
      ρ a * Function.rightLim (q b).val 0 = (eig a - eig b) *
        ((d a - ∫ u in 0..1, q a u) * Function.rightLim (q b).val 0 +
          Function.rightLim (q a).val 0 * (d b - ∫ u in 0..1, q b u))) (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)) := by
…

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

theorem OAI.InvariantIsing.canonical_groups_identification_of_symbols_rootWard line 94

Source documentation

The symbols, path sum and root Ward equations determine the complete canonical spectral family, including its diagonal.

theorem canonical_groups_identification_of_symbols_rootWard (ρ 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)))
    (hsum : ∀ᵐ s ∂pathMeasure, ∑ a, q a s = p s)
    (hward : ∀ a b, ρ b * Function.rightLim (q a).val 0 -
      ρ a * Function.rightLim (q b).val 0 = (eig a - eig b) *
        ((d a - ∫ u in 0..1, q a u) * Function.rightLim (q b).val 0 +
          Function.rightLim (q a).val 0 * (d b - ∫ u in 0..1, q b u))) :
    (∀ a, d a = spectralGroupDiagonal ρ eig hρ hρsum p a) ∧
      ∀ᵐ s ∂pathMeasure, ∀ a, q a s = spectralGroupPath ρ eig hρ hρsum p a s :=
…

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