OAI/Analysis/KadisonKastler/CentralSpectralContraction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform contraction toward the center of a von Neumann algebra

  1. theorem OAI.KadisonKastler.average_real_smul line 18
  2. theorem OAI.KadisonKastler.spectral_average_upper line 23
  3. theorem OAI.KadisonKastler.spectral_average_lower line 34
  4. theorem OAI.KadisonKastler.central_interval_norm_bound line 46
  5. theorem OAI.KadisonKastler.exists_central_spectral_contraction line 70

    Source documentation

    A central sign projection selects the midpoint of the reduced spectral interval. The contraction is uniform in the algebra and representation.

    theorem exists_central_spectral_contraction (x : Algebra M) (hx : IsSelfAdjoint x) :
    ∃ (A : FiniteInnerAverage M) (c : Algebra (concreteCenter M)),
      IsSelfAdjoint c ∧
      ‖A.apply x.val - c.val‖ ≤ (3 / 4 : ℝ) * ‖x‖ := by
…

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