ResolventCutBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A bounded resolvent estimate for separated spectral cuts

The estimate uses a right inverse only on one spectral subspace. All operators in the proof are bounded; the later spectral representation provides these identities for the resolvents of the modular operators.

theorem OAI.KadisonKastler.norm_separated_cuts_le line 19

theorem OAI.KadisonKastler.norm_logarithmically_separated_cuts_le line 52

Source documentation

A convenient uniform constant for the resolvent cuts separated by one unit of logarithmic spectrum.

theorem norm_logarithmically_separated_cuts_le
    (A B P Q R : H →L[ℂ] H) {e : ℝ} (he : 0 ≤ e)
    (hQ : ‖Q‖ ≤ 1)
    (hR : ‖R‖ ≤ 1 + Real.exp (-(1 / 2 : ℝ)))
    (hQB : ‖Q * B‖ ≤ Real.exp (-(1 / 2 : ℝ)) / (1 + Real.exp (-(1 / 2 : ℝ))))
    (hAB : ‖A - B‖ ≤ e)
    (hAR : A * R = P) (hPR : P * R = R) (hQBQ : Q * B * Q = Q * B) :
    ‖Q * P‖ ≤ ((1 + Real.exp (-(1 / 2 : ℝ))) /
      (1 - Real.exp (-(1 / 2 : ℝ)))) * e := by
…