OAI/Analysis/KadisonKastler/ScalarOrbitClosure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

From arbitrarily accurate scalar averages to a scalar in the closed orbit hull

  1. theorem OAI.KadisonKastler.exists_scalar_mem_closed_orbit line 17

    Source documentation

    The scalar values of contractive finite averages stay in a compact disk. Thus arbitrarily small scalar errors give an actual scalar in the closed hull.

    theorem exists_scalar_mem_closed_orbit (x : H →L[ℂ] H)
    (havg : ∀ ε : ℝ, 0 < ε → ∃ (A : FiniteInnerAverage M) (z : ℂ),
      ‖A.apply x - z • (1 : H →L[ℂ] H)‖ < ε) :
    ∃ z : ℂ, z • (1 : H →L[ℂ] H) ∈ closure (convexHull ℝ (innerUnitaryOrbit M x)) := by
…

    Mentions: OAI.KadisonKastler.FiniteInnerAverage, OAI.KadisonKastler.innerUnitaryOrbit