OAI/Analysis/PureInfiniteness/CrossCompressionEstimate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Off-diagonal estimates for the different copies of a spectral compressor.

  1. lemma OAI.WeakPureInfiniteness.cross_column_norm_le line 14
  2. lemma OAI.WeakPureInfiniteness.norm_cross_compression_error line 25