PositiveConeOrbitEstimate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A quantitative comparison of positive cone vectors

Acuteness applied to the quadratic action of 1 - J u J controls the distance of two positive unit vectors by their distance after a commutant unitary. This is a local vector estimate; no state representation or homogeneity theorem is assumed here.

theorem OAI.KadisonKastler.positiveCone_unitary_orbit_norm_sq_le line 23

theorem OAI.KadisonKastler.positiveCone_norm_sub_le_of_orbit_bound line 91

Source documentation

The orbit comparison gives a square-root modulus on positive unit vectors.

theorem positiveCone_norm_sub_le_of_orbit_bound
    (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_eq_of_orbit_distance_zero line 109

Source documentation

Zero distance between the two commutant-unitary orbits forces equality, without needing a minimizing unitary.

theorem positiveCone_eq_of_orbit_distance_zero
    (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