PositiveConeOrthogonality.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal positive vectors have orthogonal algebra supports

The quadratic positivity of the generated modular cone suffices for this step of Araki's Theorem 4(7), Pacific J. Math. 50 (1974), 309–354. No self-duality or positive decomposition is assumed.

theorem OAI.KadisonKastler.linear_coefficient_eq_zero line 25
theorem OAI.KadisonKastler.positiveCone_inner_left_eq_zero_of_dual_orthogonal line 31
theorem OAI.KadisonKastler.positiveCone_inner_left_eq_zero_of_orthogonal line 84

theorem OAI.KadisonKastler.positiveCone_support_kills_dual_of_orthogonal line 98

Source documentation

A positive support also kills orthogonal fixed vectors in the dual cone.

theorem positiveCone_support_kills_dual_of_orthogonal
    (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 ξ=ξ)
    {η ζ : H} (hηJ : J η=η)
    (hdual : ∀ v ∈ modularPositiveCone (M := M) J ξ, 0 ≤ inner ℝ η v)
…

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

theorem OAI.KadisonKastler.positiveCone_support_kills_of_orthogonal line 129

Source documentation

The support of one positive vector kills every orthogonal positive vector.

theorem positiveCone_support_kills_of_orthogonal
    (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 ξ=ξ)
    (hpos : ∀ a : Algebra M, 0 ≤ inner ℝ ξ (modularQuadratic J a ξ))
    {η ζ : H} (hη : η ∈ modularPositiveCone (M := M) J ξ)
…

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

theorem OAI.KadisonKastler.positiveCone_support_mul_eq_zero_of_orthogonal line 162

Source documentation

Both support projections are orthogonal in the ambient algebra.

theorem positiveCone_support_mul_eq_zero_of_orthogonal
    (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 ξ=ξ)
    (hpos : ∀ a : Algebra M, 0 ≤ inner ℝ ξ (modularQuadratic J a ξ))
    {η ζ : H} (hη : η ∈ modularPositiveCone (M := M) J ξ)
…

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