OAI/Analysis/KadisonKastler/ModularSeparatedCuts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.norm_modular_separated_cuts_le line 15

   Source documentation

   The cut comparison is proved from a one-algebra spectral resolution and the independently proved two-algebra graph estimate.

   theorem norm_modular_separated_cuts_le
       {M N : VonNeumannAlgebra H} {Ω : H}
       (m : ModularSpectralResolution M Ω) (n : ModularSpectralResolution N Ω)
       (J : H ≃ₗᵢ⋆[ℂ] H) {e : ℝ} (he : 0 ≤ e)
       (hgraph : ∀ c : ℝ, 0 < c →
         ‖rescaledGraphProjection M J Ω c - rescaledGraphProjection N J Ω c‖ ≤ e)
       (a : ℝ) :
       ‖(1 - n.upperCut (a - 1 / 2)) * m.upperCut (a + 1 / 2)‖ ≤
         ((1 + Real.exp (-(1 / 2 : ℝ))) / (1 - Real.exp (-(1 / 2 : ℝ)))) * e := by
   …

   Mentions: OAI.KadisonKastler.ModularSpectralResolution, OAI.KadisonKastler.rescaledGraphProjection