PositiveConeSelfDual.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Self-duality on the conjugation-fixed real Hilbert space

A dual residual orthogonal to a positive vector is killed by its support. Compressing the reference vector to the complementary corner then forces that residual to vanish. Cyclicity of the reference is the only density hypothesis. This proves the local self-duality needed for state estimates.

theorem OAI.KadisonKastler.positiveCone_dual_eq_zero_of_reference_orthogonal line 25
theorem OAI.KadisonKastler.modularPositiveCone_mem_of_dual line 42

theorem OAI.KadisonKastler.modularPositiveCone_mem_iff_dual line 89

Source documentation

Self-duality is stated on the real fixed space, without introducing a new type or any claim that the complex Hilbert space is ordered.

theorem modularPositiveCone_mem_iff_dual
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (hright : ∀ a : Algebra M, conjugationOperator J a.val ∈ M.commutant)
    (hleft : ∀ a : Algebra M.commutant, conjugationOperator J a.val ∈ M)
    (ξ : H) (hξ : J ξ=ξ) (hcyc : DenseRange (algebraVectorMap M ξ))
    (hpos : ∀ a : Algebra M, 0 ≤ inner ℝ ξ (modularQuadratic J a ξ)) (x : H) :
    x ∈ modularPositiveCone (M := M) J ξ ↔
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.modularQuadratic, OAI.KadisonKastler.modularPositiveCone