OAI/Analysis/PureInfiniteness/NormalizedSeparatingSequence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The normalized separating vector and its actual positive functional.

  1. lemma OAI.WeakPureInfiniteness.separatingSequence_ne_zero line 15
  2. def OAI.WeakPureInfiniteness.normalizedSeparatingSequence line 24
  3. lemma OAI.WeakPureInfiniteness.normalizedSeparatingSequence_norm line 27
  4. lemma OAI.WeakPureInfiniteness.normalizedSeparatingSequence_separating line 34
  5. def OAI.WeakPureInfiniteness.vectorPositiveFunctional line 48
  6. lemma OAI.WeakPureInfiniteness.vectorPositiveFunctional_apply line 52
  7. def OAI.WeakPureInfiniteness.sequenceStandardGNSData line 56

    Source documentation

    A dense sequence gives a standard representation with a separating vector.

    def sequenceStandardGNSData (π : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (ξ : H) (hξ : ‖ξ‖ = 1) (d : ℕ → H) (hd : DenseRange d) :
    CyclicSeparatingData (gnsHilbert (vectorPositiveFunctional (sequenceAmplification π)
      (normalizedSeparatingSequence ξ d))) :=
…

    Mentions: OAI.WeakPureInfiniteness.gnsHilbert, OAI.WeakPureInfiniteness.vectorPositiveFunctional, OAI.WeakPureInfiniteness.sequenceAmplification, OAI.WeakPureInfiniteness.normalizedSeparatingSequence