GraphRowSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Selecting a replicated row with a uniform fourth-moment cost

The row length cancels against the small left vector-state variance of the flattened element. The resulting constant is independent of the rescaling parameter and the row length.

theorem OAI.KadisonKastler.rowLimit_numeric_bound line 22

theorem OAI.KadisonKastler.exists_matrixGraphRow_cost_le line 42

Source documentation

For every flattened element, an actual finite matrix-orbit row has uniformly bounded cost. The row length is exactly the square rescaling.

theorem exists_matrixGraphRow_cost_le
    (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 : ∀ T ∈ M, (∀ n a, a ∈ (E n).algebra → a * T = T * a) →
      ∃ c : ℂ, T = c • (1 : H →L[ℂ] H))
    (hc : ∀ n a, a ∈ (E n).algebra → ∀ x ∈ M,
      inner ℂ Ω ((a * x) Ω) = inner ℂ Ω ((x * a) Ω))
    {k : ℕ} (hk : 0 < k) (z : H →L[ℂ] H) (hz : z ∈ M)
    (hznorm : ‖z‖ ≤ 128) (hzsize : ‖z Ω‖ ^ 2 + k * ‖star z Ω‖ ^ 2 ≤ 240) :
    ∃ j, ∃ ω : Fin k → SignedPermutation (Fin (d j)),
…

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