OAI/Analysis/PureInfiniteness/ScalarSampling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The concrete return column and scalar sample matrices used by the joint spectral compression. All formulas are identities in finite matrix algebras.

  1. def OAI.WeakPureInfiniteness.sqrtColumn line 17
  2. def OAI.WeakPureInfiniteness.scalarSample line 20
  3. lemma OAI.WeakPureInfiniteness.sqrtColumn_gram line 24
  4. lemma OAI.WeakPureInfiniteness.sqrtColumn_norm_le_one line 34
  5. lemma OAI.WeakPureInfiniteness.scalarSample_mul_sqrtColumn line 43
  6. lemma OAI.WeakPureInfiniteness.columnReturn_scalarSample line 49
  7. lemma OAI.WeakPureInfiniteness.scalarSample_square line 64
  8. lemma OAI.WeakPureInfiniteness.scalarSample_selfAdjoint line 74
  9. lemma OAI.WeakPureInfiniteness.scalarSample_commute_diagonal line 84
  10. lemma OAI.WeakPureInfiniteness.diagonal_of_offdiagonal_zero line 94