RescaledGraphSignal.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Selecting a normalized vector in a rescaled graph

If a nonzero operator is supported on the closed graph, one of the defining graph vectors retains more than half its operator norm. The algebra element can then be rescaled to make its graph vector a unit vector. This is the signal-selection step used before finite averaging.

theorem OAI.KadisonKastler.exists_normalized_rescaledGraph_signal line 22

Source documentation

A graph-supported nonzero operator has a normalized defining graph vector on which it retains more than half its norm.

theorem exists_normalized_rescaledGraph_signal
    (P : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) (hT : T ≠ 0)
    (hsupport : T * rescaledGraphProjection P J Ω c = T) :
    ∃ x : Algebra P, ‖rescaledGraphVector J Ω c x.val‖ = 1 ∧
      ‖T‖ / 2 < ‖T (rescaledGraphVector J Ω c x.val)‖ := by
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.rescaledGraphProjection, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.rescaledGraphVector