OAI/Probability/InvariantIsing/Spectral/SpectralFubini.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InvariantIsing.integral_spectralDensity_CDF_fubini line 19

   Source documentation

   The layer-cake calculation in manuscript rot:function-path.

   theorem integral_spectralDensity_CDF_fubini (ρ 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 {u | p u ≤ r}) =
         ∫ u, (∫ r in max q (p u)..1, spectralPathDensity ρ eig hρ hρsum p a r) ∂pathMeasure := by
   …

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

2. theorem OAI.InvariantIsing.spectralGroupSymbol_eq_CDF_integral line 61
3. theorem OAI.InvariantIsing.spectralGroupSymbol_eq_projectedResolvent line 139

   Source documentation

   The full reconstructed-symbol identity in manuscript rot:function-path.

   theorem spectralGroupSymbol_eq_projectedResolvent (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
       (hρsum : ∑ a, ρ a = 1) (p : OverlapPath) (a : ι) {s : ℝ}
       (hs : s ∈ Icc (0 : ℝ) 1) :
       pathSymbol (spectralGroupDiagonal ρ eig hρ hρsum p a)
         (spectralGroupPath ρ eig hρ hρsum p a) s =
         projectedResolvent ρ eig hρ hρsum a (deficit p (p s)) := by
   …

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