GraphDirectionalBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Directional graph estimates from actual row approximants

A bounded detecting row in the first algebra is compared with one row in the second algebra. Only the stated rectangular approximation is used; no amplification of ordinary Kadison--Kastler distance is assumed.

theorem OAI.KadisonKastler.graphProjectionDefect_le_of_row line 23

Source documentation

A detecting row and its actual approximant bound the directional orthogonal graph defect.

theorem graphProjectionDefect_le_of_row
    (M N : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (hΩ : ‖Ω‖ = 1)
    {k : ℕ} (hk : 0 < k) {γ : ℝ} (hγ : 0 ≤ γ)
    (X Z : Fin k → H →L[ℂ] H) (hX : ∀ i, X i ∈ M) (hZ : ∀ i, Z i ∈ N)
    (hXnorm : ‖operatorRow X‖ ≤ 131072)
    (happrox : ‖operatorRow X - operatorRow Z‖ ≤ γ * ‖operatorRow X‖)
    (hsignal : ‖(1 - rescaledGraphProjection N J Ω (Real.sqrt (k : ℝ))) *
        rescaledGraphProjection M J Ω (Real.sqrt (k : ℝ))‖ / 16 ≤
      finiteRMS (fun i => ((1 - rescaledGraphProjection N J Ω (Real.sqrt (k : ℝ))) *
        rescaledGraphProjection M J Ω (Real.sqrt (k : ℝ)))
          (rescaledGraphVector J Ω (Real.sqrt (k : ℝ)) (X i)))) :
    ‖(1 - rescaledGraphProjection N J Ω (Real.sqrt (k : ℝ))) *
…

Mentions: OAI.KadisonKastler.operatorRow, OAI.KadisonKastler.rescaledGraphProjection, OAI.KadisonKastler.finiteRMS, OAI.KadisonKastler.rescaledGraphVector

theorem OAI.KadisonKastler.norm_graphProjectionDefect_le_of_row_approx line 83

Source documentation

Actual matrix-orbit flattening and complete row approximation give the directional bound at every integer square rescaling.

theorem norm_graphProjectionDefect_le_of_row_approx
    (M N : 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)
    (hcommM : ∀ j a, a ∈ (E j).algebra → conjugationOperator J (star a) ∈ M.commutant)
    (hcommN : ∀ j a, a ∈ (E j).algebra → conjugationOperator J (star a) ∈ N.commutant)
…

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