OAI/Analysis/PureInfiniteness/CompressionNorms.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Norm identities that return the finite matrix estimates to the original nonunital algebra and identify the two sampled moments.

  1. lemma OAI.WeakPureInfiniteness.unitizationOneByOne_compression_norm line 16
  2. lemma OAI.WeakPureInfiniteness.unitizationOneByOne_commutator_norm line 24
  3. lemma OAI.WeakPureInfiniteness.scalarSample_first_moment_norm line 33
  4. lemma OAI.WeakPureInfiniteness.scalarSample_second_moment_norm line 43