OAI/Analysis/OperatorAlgebra/FinitePredualConjugation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Unitary conjugation preserves the finite operator predual, contractively, and carries a vector functional to the functional of the transformed vectors.

  1. def OAI.WeakPureInfiniteness.conjugatedOperator line 16
  2. lemma OAI.WeakPureInfiniteness.conjugatedOperator_apply line 19
  3. def OAI.WeakPureInfiniteness.predualUnitaryAmbient line 22
  4. lemma OAI.WeakPureInfiniteness.predualUnitaryAmbient_coefficient line 34
  5. lemma OAI.WeakPureInfiniteness.predualUnitaryAmbient_mem line 40
  6. def OAI.WeakPureInfiniteness.finitePredualUnitary line 54
  7. lemma OAI.WeakPureInfiniteness.finitePredualUnitary_apply line 59
  8. lemma OAI.WeakPureInfiniteness.finitePredualUnitary_coefficient line 63