OAI/Analysis/KadisonKastler/SupportSpanNorm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform norm bounds on finite initial sums extend to the full central support. The argument uses norm density, without normality of a representation.

  1. theorem OAI.KadisonKastler.finiteSupportSum_fixes_of_subset line 18
  2. theorem OAI.KadisonKastler.support_span_has_finite_support line 29
  3. theorem OAI.KadisonKastler.norm_comp_partialSupportProjection_le line 61