OAI/Analysis/WeakInfiniteness/TensorHilbertSum.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.tensorSequence line 22
  2. lemma OAI.WeakPureInfiniteness.tensorSequence_apply line 27
  3. def OAI.WeakPureInfiniteness.tensorSequenceBilinear line 30
  4. def OAI.WeakPureInfiniteness.tensorToHilbertSumMap line 35
  5. lemma OAI.WeakPureInfiniteness.tensorToHilbertSumMap_tmul line 39
  6. lemma OAI.WeakPureInfiniteness.tensorToHilbertSumMap_inner line 42
  7. def OAI.WeakPureInfiniteness.tensorToHilbertSum line 57
  8. lemma OAI.WeakPureInfiniteness.tensorToHilbertSum_intertwining line 64
  9. theorem OAI.WeakPureInfiniteness.norm_freeTensor_sum_le line 79