OAI/Probability/InvariantIsing/Spectral/SpectralEnergy.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.finiteSpectralSlope line 20
2. def OAI.InvariantIsing.finiteThermalScalar line 24
3. def OAI.InvariantIsing.finiteInteractionEnergy line 28
4. theorem OAI.InvariantIsing.continuous_finiteR line 32
5. theorem OAI.InvariantIsing.continuous_finiteSpectralSlope line 45
6. theorem OAI.InvariantIsing.finiteSpectralSlope_zero line 50
7. theorem OAI.InvariantIsing.finiteSpectralSlope_bounds line 58
8. theorem OAI.InvariantIsing.sum_eig_projectedResolvent line 77
9. theorem OAI.InvariantIsing.hasDerivWithinAt_mul_finiteR_nonneg line 100
10. theorem OAI.InvariantIsing.finiteSpectralSlope_monotoneOn line 112
11. theorem OAI.InvariantIsing.hasDerivWithinAt_finiteThermalScalar line 136
12. theorem OAI.InvariantIsing.finiteInteractionEnergy_mono_deficit line 159
13. theorem OAI.InvariantIsing.finiteInteractionEnergy_mono_tail line 177

    Source documentation

    The energy comparison in Section 4 follows from the upper-tail order, including paths with atoms.

    theorem finiteInteractionEnergy_mono_tail (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
        (hρsum : ∑ a, ρ a = 1) {t : ℝ} (ht : 0 ≤ t) (p q : OverlapPath)
        (htail : ∀ s ∈ Icc (0 : ℝ) 1, pathTail q s ≤ pathTail p s) :
        finiteInteractionEnergy ρ eig hρ hρsum t p ≤ finiteInteractionEnergy ρ eig hρ hρsum t q := by
    …

    Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.pathTail, OAI.InvariantIsing.finiteInteractionEnergy

14. theorem OAI.InvariantIsing.abs_finiteInteractionEnergy_le line 184