OAI/Analysis/WeakInfiniteness/FiniteDiagonalState.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakPureInfiniteness.tensor_inner_smul_smul line 14
  2. def OAI.WeakPureInfiniteness.finiteLeftRegularIsometry line 26
  3. def OAI.WeakPureInfiniteness.finiteLeftRegular line 38
  4. lemma OAI.WeakPureInfiniteness.finiteLeftRegular_apply line 44
  5. lemma OAI.WeakPureInfiniteness.finiteLeftRegular_single line 48
  6. def OAI.WeakPureInfiniteness.finiteDiagonalVector line 54
  7. lemma OAI.WeakPureInfiniteness.inner_finiteDiagonalVector_translate line 58
  8. lemma OAI.WeakPureInfiniteness.inner_finiteDiagonalVector_self line 79
  9. def OAI.WeakPureInfiniteness.normalizedFiniteDiagonalVector line 84
  10. lemma OAI.WeakPureInfiniteness.normalizedFiniteDiagonalVector_inner_translate line 88
  11. lemma OAI.WeakPureInfiniteness.norm_normalizedFiniteDiagonalVector line 119