FlattenedGraphVector.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A bounded operator retaining the rescaled graph defect

The defining graph vector is normalized, averaged over the actual finite matrix orbits, sampled with independent signs, and spectrally clipped. All bounds concern the same resulting algebra element.

theorem OAI.KadisonKastler.normalizedSignSum_mem line 27
theorem OAI.KadisonKastler.matrixOrbitSample_mem line 38

theorem OAI.KadisonKastler.exists_bounded_rescaledGraph_signal line 51

Source documentation

A nonzero graph-supported operator has one uniformly bounded algebra vector which retains a fixed fraction of its norm. The matrix actions are the actual common left/right actions on the graph.

theorem exists_bounded_rescaledGraph_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 : 1 ≤ k)
    (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) (hT : T ≠ 0)
…

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