OAI/Analysis/OperatorAlgebra/HilbertDualOperators.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The concrete opposite-algebra representation on the conjugate Hilbert space, needed for the spatial vector functionals of finite density roots.

  1. def OAI.WeakPureInfiniteness.hilbertDualOperator line 15
  2. lemma OAI.WeakPureInfiniteness.hilbertDualOperator_apply line 18
  3. lemma OAI.WeakPureInfiniteness.hilbertDualOperator_toDual line 21
  4. lemma OAI.WeakPureInfiniteness.hilbertDualOperator_star line 27
  5. def OAI.WeakPureInfiniteness.hilbertDualRepresentation line 39

    Source documentation

    Precomposition reverses multiplication, so the conjugate Hilbert space carries an actual star representation of the opposite operator algebra.

    def hilbertDualRepresentation :
    (H →L[ℂ] H)ᵐᵒᵖ →⋆ₐ[ℂ] (StrongDual ℂ H →L[ℂ] StrongDual ℂ H) where
…