OAI/Analysis/KadisonKastler/RegularIntervalCutoffs.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Compact interval cutoffs for regular vectors

These are elementary support and approximation facts for the actual indicator projections. They do not require a commutant theorem.

  1. theorem OAI.KadisonKastler.regularIndicator_translate_eq_of_support line 23
  2. theorem OAI.KadisonKastler.regularIndicator_translate_zero_of_support line 44
  3. theorem OAI.KadisonKastler.regularInterval_translate_eq line 67
  4. theorem OAI.KadisonKastler.regularInterval_translate_zero line 80
  5. theorem OAI.KadisonKastler.regularIntervalProjection_tendsto line 96

    Source documentation

    Symmetric interval projections converge strongly to the identity.

    theorem regularIntervalProjection_tendsto (f : RegularCoreHilbert H) :
    Tendsto (fun n : ℕ => regularIndicatorProjection
      (Set.Icc (-(n : ℝ)) (n : ℝ)) measurableSet_Icc f) atTop (𝓝 f) := by
…

    Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularIndicatorProjection