OAI/Analysis/KadisonKastler/BoundedSpectralApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded coefficients in the constructed finite spectral approximations

The dyadic spectral intervals remain inside their initial norm bounds. This records the coefficient bound needed by the threshold-cut argument.

  1. theorem OAI.Generator.Tracial.SpectralInterval.level_nested line 21
  2. theorem OAI.Generator.Tracial.exists_bounded_spectral_approximation line 38