OAI/Analysis/Nuclearity/PositiveConeNullIdeal.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The closed two-sided ideal occurring in KR02 Lemma 7.17(ii). It is constructed from square nullspaces of positive functionals; stability under coefficient conjugation supplies right multiplication and the star law.

  1. def OAI.WeakPureInfiniteness.conjugatePositiveFunctional line 18
  2. lemma OAI.WeakPureInfiniteness.conjugatePositiveFunctional_apply line 25
  3. def OAI.WeakPureInfiniteness.commonSquareNull line 28
  4. lemma OAI.WeakPureInfiniteness.positiveFunctional_mixed_eq_zero line 31
  5. lemma OAI.WeakPureInfiniteness.commonSquareNull_add line 37
  6. lemma OAI.WeakPureInfiniteness.commonSquareNull_smul line 47
  7. lemma OAI.WeakPureInfiniteness.commonSquareNull_mul_right line 52
  8. lemma OAI.WeakPureInfiniteness.commonSquareNull_star line 59
  9. lemma OAI.WeakPureInfiniteness.commonSquareNull_mul_left line 68
  10. lemma OAI.WeakPureInfiniteness.isClosed_commonSquareNull line 75
  11. def OAI.WeakPureInfiniteness.commonSquareNullIdeal line 87

    Source documentation

    The common square nullspace is a genuine closed star ideal, including for nonunital algebras. No ideal-generation hypothesis is built into the definition.

    def commonSquareNullIdeal (K : Set (A →ₚ[ℂ] ℂ))
    (hconj : ∀ φ ∈ K, ∀ d : A, conjugatePositiveFunctional φ d ∈ K) :
    NonunitalClosedIdeal.Ideal A where
…

    Mentions: OAI.WeakPureInfiniteness.conjugatePositiveFunctional, OAI.NonunitalClosedIdeal.Ideal

  12. lemma OAI.WeakPureInfiniteness.commonSquareNullIdeal_mem_iff line 100
  13. lemma OAI.WeakPureInfiniteness.positiveFunctional_vanishes_commonSquareNull line 104
  14. lemma OAI.WeakPureInfiniteness.positiveLinearMap_ext_selfAdjoint line 110
  15. def OAI.WeakPureInfiniteness.complexifyWeakPositive line 116
  16. lemma OAI.WeakPureInfiniteness.complexifyWeakPositive_apply line 120
  17. def OAI.WeakPureInfiniteness.positiveConeComplexification line 125
  18. lemma OAI.WeakPureInfiniteness.positiveConeComplexification_conjugate line 130
  19. def OAI.WeakPureInfiniteness.realPositiveConeNullIdeal line 146

    Source documentation

    The closed ideal attached to the real weak-star cone in Lemma 7.17(ii).

    def realPositiveConeNullIdeal
    (K : Set (WeakDual ℝ (selfAdjoint A)))
    (hpositive : ∀ φ ∈ K, ∀ a : selfAdjoint A, 0 ≤ (a : A) → 0 ≤ φ a)
    (hconj : ∀ φ ∈ K, ∀ d : A, conjugateRealFunctional φ d ∈ K) :
    NonunitalClosedIdeal.Ideal A :=
…

    Mentions: OAI.WeakPureInfiniteness.conjugateRealFunctional, OAI.NonunitalClosedIdeal.Ideal

  20. lemma OAI.WeakPureInfiniteness.mem_realPositiveConeNullIdeal_iff line 154