GraphResolventCompression.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Contractive compression of the actual graph projection

The first diagonal entry is the bounded graph resolvent. Its comparison follows directly from the norm comparison of the whole graph projections.

theorem OAI.KadisonKastler.norm_graph_operatorEntry_le line 18
def OAI.KadisonKastler.graphResolvent line 28
theorem OAI.KadisonKastler.norm_graphResolvent_sub_le line 32

theorem OAI.KadisonKastler.norm_cut_product_of_graph_bound line 46

Source documentation

Once the spectral theorem gives the cut-restricted inverse, the separated-cut bound uses only the proved graph comparison.

theorem norm_cut_product_of_graph_bound
    (M N : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    (P Q R : H →L[ℂ] H) {e : ℝ} (he : 0 ≤ e)
    (hgraph : ‖rescaledGraphProjection M J Ω c - rescaledGraphProjection N J Ω c‖ ≤ e)
    (hQ : ‖Q‖ ≤ 1) (hR : ‖R‖ ≤ 1 + Real.exp (-(1 / 2 : ℝ)))
    (hQB : ‖Q * graphResolvent N J Ω c‖ ≤
      Real.exp (-(1 / 2 : ℝ)) / (1 + Real.exp (-(1 / 2 : ℝ))))
    (hAR : graphResolvent M J Ω c * R = P)
    (hPR : P * R = R)
    (hQBQ : Q * graphResolvent N J Ω c * Q = Q * graphResolvent N J Ω c) :
    ‖Q * P‖ ≤ ((1 + Real.exp (-(1 / 2 : ℝ))) /
      (1 - Real.exp (-(1 / 2 : ℝ)))) * e :=
…

Mentions: OAI.KadisonKastler.rescaledGraphProjection, OAI.KadisonKastler.graphResolvent