OAI/Analysis/KadisonKastler/DominatedVectorState.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Bounded Radon--Nikodym operators for vector states

Domination of the two orbit norms extends the algebraic orbit map to a bounded operator in the commutant. Its square gives the positive Radon--Nikodym operator on the original cyclic representation.

  1. def OAI.KadisonKastler.dominatedVectorIntertwiner line 19
  2. theorem OAI.KadisonKastler.dominatedVectorIntertwiner_orbit line 26
  3. theorem OAI.KadisonKastler.dominatedVectorIntertwiner_vector line 31
  4. theorem OAI.KadisonKastler.dominatedVectorIntertwiner_norm line 35
  5. theorem OAI.KadisonKastler.dominatedVectorIntertwiner_commutant line 40
  6. theorem OAI.KadisonKastler.exists_positive_vectorState_derivative line 59
  7. theorem OAI.KadisonKastler.commutant_operator_eq_of_vector_coefficients line 77
  8. theorem OAI.KadisonKastler.exists_positive_vectorState_derivative_of_quadratic_bound line 116

    Source documentation

    The quadratic state inequality supplies the orbit norm bound directly.

    theorem exists_positive_vectorState_derivative_of_quadratic_bound
    (D : ℝ) (hD : 0 ≤ D)
    (hdom : ∀ a : Algebra M,
      (inner ℂ η ((star a*a).val η)).re ≤ D * (inner ℂ ξ ((star a*a).val ξ)).re) :
    ∃ T : H →L[ℂ] H, T ∈ M.commutant ∧ 0 ≤ T ∧ ‖T‖ ≤ D ∧
      ∀ a : Algebra M, inner ℂ η (a.val η) = inner ℂ ξ (T (a.val ξ)) := by
…

    Mentions: OAI.KadisonKastler.Algebra