OAI/Analysis/KadisonKastler/CentralLocalizationMinimum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compactness assembles the finite support rows into the localized norm bound used by Paulsen's minimal-family argument. No normality of the auxiliary representation is needed: the finite sums are on the original space.

  1. theorem OAI.KadisonKastler.representationRowAverage_reindex line 20
  2. theorem OAI.KadisonKastler.norm_comp_finiteSupportSum_mono line 27
  3. theorem OAI.KadisonKastler.exists_central_localized_norm_le line 44