FlattenedGraphRow.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A bounded replicated row retaining the graph signal

A single cutoff of the row square preserves algebra membership and loses at most one thirty-second of the graph signal in normalized mean square. The cutoff and the row norm are independent of the row length.

theorem OAI.KadisonKastler.clippedGraphRow_mem line 25

theorem OAI.KadisonKastler.clippedGraphRow_error_le line 40

Source documentation

The common row cutoff has small graph error at the fixed cutoff.

theorem clippedGraphRow_error_le {k : ℕ} (hk : 0 < k)
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (Y : Fin k → H →L[ℂ] H)
    (hcost : graphRowCost Ω Y ≤ 16777216) :
    finiteRMS (fun i => rescaledGraphVector J Ω (Real.sqrt (k : ℝ))
      (Y i - clippedGraphRow 131072 Y i)) ≤ 1 / 32 := by
…

Mentions: OAI.KadisonKastler.graphRowCost, OAI.KadisonKastler.finiteRMS, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.clippedGraphRow

theorem OAI.KadisonKastler.clippedGraphRow_signal_le line 53

Source documentation

A uniformly nonzero row signal survives the same cutoff used for its operator norm bound.

theorem clippedGraphRow_signal_le {k : ℕ} (hk : 0 < k)
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
    (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H)
    (Y : Fin k → H →L[ℂ] H) (hcost : graphRowCost Ω Y ≤ 16777216)
    (hsignal : ‖T‖ / 8 ≤ finiteRMS (fun i =>
      T (rescaledGraphVector J Ω (Real.sqrt (k : ℝ)) (Y i)))) :
    ‖T‖ / 16 ≤ finiteRMS (fun i =>
      T (rescaledGraphVector J Ω (Real.sqrt (k : ℝ)) (clippedGraphRow 131072 Y i))) := by
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.graphRowCost, OAI.KadisonKastler.finiteRMS, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.clippedGraphRow

theorem OAI.KadisonKastler.matrixGraphRow_signal_eq line 85

Source documentation

Every left matrix translate of an algebra element has exactly the same graph signal when the actual graph action commutes with the defect.

theorem matrixGraphRow_signal_eq (M : VonNeumannAlgebra H)
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J) (Ω : H) (c : ℝ)
    (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) {d : ℕ}
    (E : Generator.MatrixUnitSystem (Fin d) (H →L[ℂ] H))
    (z : H →L[ℂ] H) (hz : z ∈ M)
    (hcomm : ∀ a, a ∈ E.algebra → conjugationOperator J (star a) ∈ M.commutant)
    (hvector : ∀ a, a ∈ E.algebra → conjugationOperator J (star a) Ω = a Ω)
    (hinvariant : ∀ u : unitary (H →L[ℂ] H), (u : H →L[ℂ] H) ∈ E.algebra →
      T * (rescaledGraphAction J hJ u 1 : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) =
        (rescaledGraphAction J hJ u 1 : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) * T)
    {I : Type*} (ω : I → SignedPermutation (Fin d)) (i : I) :
    ‖T (rescaledGraphVector J Ω c (matrixGraphRow E z ω i))‖ =
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert, OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.rescaledGraphAction, OAI.KadisonKastler.SignedPermutation, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.matrixGraphRow