OAI/Analysis/PureInfiniteness/FiniteCompressionError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite compression estimate in the joint spectral argument. The row error controls preservation by the resulting contractive compression.

  1. lemma OAI.WeakPureInfiniteness.norm_row_column_le_one line 14
  2. lemma OAI.WeakPureInfiniteness.norm_finite_compression_error line 20
  3. lemma OAI.WeakPureInfiniteness.norm_finite_compression_preservation line 39