MatrixVectorPreparation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Nearby positive matrix-central vectors

The proved Powers–Størmer inequality turns the two-corner state comparison into the vector comparison required by finite-matrix refinement. Connes–Størmer homogeneity remains the explicit published premise.

theorem OAI.KadisonKastler.TypeIIIFactor.exists_matrix_vector_of_projection_gap line 25

theorem OAI.KadisonKastler.TypeIIIFactor.exists_matrix_stage_near_projection line 51

Source documentation

The comparison matrix is packaged as a concrete finite stage.

theorem TypeIIIFactor.exists_matrix_stage_near_projection
    (hM : TypeIIIFactor M) (hhom : FaithfulVectorStateHomogeneity M)
    (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 ξ=ξ) (hunit : ‖ξ‖=1)
    (hsep : Function.Injective (algebraVectorMap M ξ))
    (hpos : ∀ a : Algebra M, 0 ≤ inner ℝ ξ (modularQuadratic J a ξ))
    (p : AlgebraProjection M) (hp0 : p.val≠0) (hp1 : p.val≠1)
    (hgap : ‖p.val.val ξ-conjugationOperator J p.val.val ξ‖ < 1)
    (ε : ℝ) (hε : 0 < ε)
    (hsmall : ‖p.val.val ξ-conjugationOperator J p.val.val ξ‖ < ε^2/8) :
…

Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.FaithfulVectorStateHomogeneity, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.modularQuadratic