AffineExpectationAverage.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Averaging the two-dimensional projection expectations

Equal free joint laws give the two scalar pairings of each affine projection expectation. These determine its coefficients independently of the selected projection. Uniformly averaging the projections then recovers exactly the common scalar trace.

theorem OAI.KadisonKastler.finiteAverage_affine_projections line 24

Source documentation

Affine projection expectations with a common pair of trace values average to the scalar given by their common trace.

theorem finiteAverage_affine_projections {ι : Type*} [Fintype ι] [Nonempty ι]
    (τ : FaithfulTracialState B) (p y : ι → B)
    (hp : ∀ i, IsStarProjection (p i)) {t c d : ℂ}
    (hptrace : ∀ i, τ.toLinearMap (p i) = t) (ht0 : t ≠ 0) (ht1 : t ≠ 1)
    (hpavg : finiteAverage p = t • (1 : B))
    (hy : ∀ i, ∃ α β : ℂ, y i = α • p i + β • (1 : B))
    (htrace : ∀ i, τ.toLinearMap (y i) = c)
    (hcompressed : ∀ i, τ.toLinearMap (p i * y i) = d) :
    finiteAverage y = c • (1 : B) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.finiteAverage