OAI/Probability/InvariantIsing/Spectral/SpectralPrimitive.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InvariantIsing.pathCDF_monotone line 18
2. theorem OAI.InvariantIsing.hasDerivWithinAt_projectedResolvent_nonneg line 23
3. theorem OAI.InvariantIsing.continuousOn_projectedResolvent line 34
4. theorem OAI.InvariantIsing.integral_spectralDensity_mul_CDF line 42

   Source documentation

   The FTC step in rot:function-path, valid even when the overlap law has atoms.

   theorem integral_spectralDensity_mul_CDF (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
       (hρsum : ∑ a, ρ a = 1) (p : OverlapPath) (a : ι) {q : ℝ}
       (hq : q ∈ Icc (0 : ℝ) 1) :
       (∫ r in q..1, spectralPathDensity ρ eig hρ hρsum p a r *
         pathMeasure.real {s | p s ≤ r}) =
         projectedResolvent ρ eig hρ hρsum a (deficit p q) := by
   …

   Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.spectralPathDensity, OAI.InvariantIsing.projectedResolvent