TracialSpectralAveraging.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite matrix averaging of rounded spectral sums

theorem OAI.KadisonKastler.exists_scalar_average_of_rounded_partition line 20

Source documentation

A common matrix-algebra remainder controls the norm error of a whole spectral sum after one finite average.

theorem exists_scalar_average_of_rounded_partition (τ : TracialRepresentation M)
    (Q : CornerPartition (identityProjection M)) (q : Fin Q.size → AlgebraProjection M)
    (hq : ∀ i, q i ≤ Q.piece i) {n : ℕ} [Nonempty (Fin n)]
    (E : MatrixUnitSystem (Fin n) (Algebra M))
    (hmem : ∀ i, (q i).val ∈ E.algebra)
    (c : Fin Q.size → ℂ) (η : ℝ)
    (hη : (τ.trace (partitionRemainder Q q hq).val).re ≤ η) :
    ∃ (A : FiniteInnerAverage M) (z : ℂ),
      ‖A.apply (∑ i, c i • (Q.piece i).val.val) - z • (1 : H →L[ℂ] H)‖ ≤
        (∑ i, ‖c i‖) * η := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.partitionRemainder, OAI.KadisonKastler.FiniteInnerAverage