BoundedGraphRow.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual bounded rows detecting the rescaled graph defect

The single bounded graph vector is replicated by independent left matrix translates, and one common spectral cutoff produces a row whose norm and retained signal have constants independent of its length.

theorem OAI.KadisonKastler.exists_bounded_graphRow_signal line 23

Source documentation

A graph-supported operator is detected by an actual bounded row of algebra elements, without any matrix amplification of ordinary distance.

theorem exists_bounded_graphRow_signal
    (M : VonNeumannAlgebra H) (Ω : H) (hΩ : ‖Ω‖ = 1)
    (d : ℕ → ℕ) (E : ∀ n, Generator.MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H))
    (hmono : Monotone (fun n => (E n).algebra))
    (hEM : ∀ n, (E n).algebra ≤ M.toStarSubalgebra)
    (hirr : ∀ A ∈ M, (∀ n a, a ∈ (E n).algebra → a * A = A * a) →
      ∃ z : ℂ, A = z • (1 : H →L[ℂ] H))
    (hc : ∀ n a, a ∈ (E n).algebra → ∀ z ∈ M,
      inner ℂ Ω ((a * z) Ω) = inner ℂ Ω ((z * a) Ω))
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    {k : ℕ} (hk : 0 < k)
    (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) (hT : T ≠ 0)
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.TomitaGraphHilbert