OAI/Analysis/KadisonSimilarity/Representation/ScalarLocalizationApproximation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniformly bounded continuous functions approximate the measurable scalar localizations needed in the central spectral model.

  1. theorem OAI.KadisonSimilarity.exists_continuous_indicator_eLpNorm_approx line 18