SelfAdjointAveraging.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Passing from self-adjoint to arbitrary operator averaging

theorem OAI.KadisonKastler.exists_scalar_average_of_selfAdjoint line 20

Source documentation

Average the real part, then the self-adjoint averaged imaginary part. The second contraction preserves the first scalar approximation.

theorem exists_scalar_average_of_selfAdjoint
    (havg : ∀ (y : Algebra M), IsSelfAdjoint y → ∀ δ : ℝ, 0 < δ →
      ∃ (A : FiniteInnerAverage M) (z : ℂ),
        ‖A.apply y.val - z • (1 : H →L[ℂ] H)‖ < δ)
    (x : Algebra M) (ε : ℝ) (hε : 0 < ε) :
    ∃ (C : FiniteInnerAverage M) (z : ℂ),
      ‖C.apply x.val - z • (1 : H →L[ℂ] H)‖ < ε := by
…

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