OAI/Analysis/KadisonKastler/TypeIIISmoothing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform exact normalizers from quantitative smoothing data

All radii and constants are chosen before the Hilbert space and factor. The smoothing hypotheses give continuous approximate inverses with controlled algebra distance and strong-star convergence.

  1. theorem OAI.KadisonKastler.exists_smoothing_radius line 23
  2. theorem OAI.KadisonKastler.uniform_typeIII_normalizer_from_smoothing line 44