SpectralGroupRoots.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Right roots of the reconstructed finite spectral-group paths. The deficit is constant below the total path's right root, including root zero.

lemma OAI.InvariantIsing.OverlapPath.rightLim_mem_unit line 15
lemma OAI.InvariantIsing.OverlapPath.rightLim_le_of_pos line 20
lemma OAI.InvariantIsing.deficit_eq_one_sub_mean_of_le_rightLim line 23
lemma OAI.InvariantIsing.deficit_eq_at_rightLim_of_le line 34
lemma OAI.InvariantIsing.spectralPathDensity_eq_at_rightLim line 42
lemma OAI.InvariantIsing.integral_spectralDensity_rightLim line 50

theorem OAI.InvariantIsing.spectralGroupPath_root_tendsto line 65

Source documentation

The reconstructed group path has the exact root prescribed by the root Ward equations, with no assumption that the total path is continuous.

theorem spectralGroupPath_root_tendsto (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
    (hρsum : ∑ a, ρ a = 1) (p : OverlapPath) (a : ι) :
    Tendsto (spectralGroupPath ρ eig hρ hρsum p a) (𝓝[>] (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.spectralGroupPath, OAI.InvariantIsing.projectedResolventDerivative

theorem OAI.InvariantIsing.spectralGroupPath_rightLim line 77
theorem OAI.InvariantIsing.sum_spectralGroupPath_rightLim line 84