OAI/Analysis/KadisonKastler/FiniteRelativeAverages.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.exists_finite_relative_scalar_average line 23

   Source documentation

   Scalar relative averaging is realized to any positive accuracy by a nonempty finite equal-weight family of actual unitaries.

   theorem exists_finite_relative_scalar_average
       (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
       (hτ : FiniteVectorTrace τ) (φ : R →⋆ₐ[ℂ] Algebra M)
       (hirr : ∀ b : Algebra M, (∀ r : R, φ r * b = b * φ r) →
         ∃ c : ℂ, b = c • (1 : Algebra M))
       (a : Algebra M) {ε : ℝ} (hε : 0 < ε) :
       ∃ n : ℕ, 0 < n ∧ ∃ u : Fin n → unitary R,
         traceTwoNorm τ ((n : ℂ)⁻¹ • ∑ i, φ (u i) * a * star (φ (u i)) -
           τ.toLinearMap a • (1 : Algebra M)) < ε := by
   …

   Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace