OAI/Analysis/KadisonKastler/OperatorMeanStar.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Adjoint preservation of operator-field averaging

  1. theorem OAI.KadisonKastler.WeakOperatorRepresentative.coefficient_star line 20
  2. theorem OAI.KadisonKastler.WeakOperatorField.coefficient_star line 35
  3. theorem OAI.KadisonKastler.WeakOperatorField.coefficientFamily_star line 44
  4. theorem OAI.KadisonKastler.ScalarBoundaryMean.operatorMean_star line 60

    Source documentation

    Adjoint preservation is derived from scalar positivity.

    theorem operatorMean_star (m : ScalarBoundaryMean α) (F : G →ᵇ WeakOperatorField (H := H) μ) :
…

    Mentions: OAI.KadisonKastler.ScalarBoundaryMean, OAI.KadisonKastler.WeakOperatorField