OAI/Analysis/KadisonKastler/ModularGraphApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Algebraic approximation of modular translates in graph norm

The full closed-graph invariance gives simultaneous approximation of a translated algebra vector and its adjoint vector by the same algebra element. These are graph-norm approximations; no operator-norm bound is asserted.

  1. theorem OAI.KadisonKastler.tomitaClosed_graph_approximate line 24

    Source documentation

    Simultaneous approximation of both coordinates of the closed graph.

    theorem tomitaClosed_graph_approximate {x y : H}
    (hxy : (x, y) ∈ (tomitaClosedLinearOperator M J Ω 1).graph)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ a : Algebra M, ‖a.val Ω - x‖ < ε ∧ ‖J (star a.val Ω) - y‖ < ε := by
…

    Mentions: OAI.KadisonKastler.tomitaClosedLinearOperator, OAI.KadisonKastler.Algebra

  2. theorem OAI.KadisonKastler.modular_translate_graph_approximate line 45