OAI/Analysis/KadisonKastler/UniformNormDetection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded-sequence tests detect a uniform operator-norm limit

This is the diagonal choice in the infinitesimal normalizer argument: equality of derivations on every element of the norm ultraproduct forces their coordinate operator norms to tend to zero.

  1. theorem OAI.KadisonKastler.exists_unitBall_half_norm_witness line 23
  2. theorem OAI.KadisonKastler.tendsto_opNorm_zero_of_bounded_sequence_tests line 31