OAI/Analysis/PureInfiniteness/CutSampleReturn.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Return of scalar samples through an exact cut Gram matrix. This is the identity used to preserve the selected elements by the finite compression.

  1. lemma OAI.WeakPureInfiniteness.diagonal_mul_sqrtColumn line 18
  2. lemma OAI.WeakPureInfiniteness.columnReturn_diagonal line 23
  3. lemma OAI.WeakPureInfiniteness.cut_diagonal_mul_scalarSample line 36
  4. lemma OAI.WeakPureInfiniteness.columnReturn_cut_sample line 45
  5. lemma OAI.WeakPureInfiniteness.finite_cut_compression_preservation line 55