OAI/Analysis/KadisonSimilarity/Representation/LocalizedFiberNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Localized quadratic estimates determine the essential bound of an operator field. Countably many vector tests suffice for the common null set.

  1. theorem OAI.KadisonSimilarity.ae_operator_norm_le_of_local_energy line 21