PublishedFieldTomiyama.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The precise Tomiyama input for the operator-field mean

Tomiyama, On the projection of norm one in W-algebras*, Proceedings of the Japan Academy 33 (1957), 608–612, Theorem 1(2), pp. 608–609, DOI 10.3792/pja/1195524885.

Only the bimodule conclusion for the constant-field inclusion is retained. The contractive retraction and its adjoint preservation are constructed in OperatorCoefficientMean and OperatorMeanStar, not assumed here.

instance OAI.KadisonKastler.operatorFieldFamilyCStar line 27
abbrev OAI.KadisonKastler.operatorFieldDiagonal line 30
Source documentation
Constant fields form the target C-star subalgebra of the expectation.
```
abbrev operatorFieldDiagonal : WeakOperatorField (H := H) μ →⋆ₐ[ℂ]
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField
def OAI.KadisonKastler.PublishedFieldTomiyama line 35
Source documentation
The constant-field specialization of Tomiyama's Theorem 1(2). This is an explicit published-input hypothesis, not an axiom.
```
def PublishedFieldTomiyama : Prop :=
…
```
def OAI.KadisonKastler.ScalarBoundaryMean.operatorBimoduleMean line 48
Source documentation
The constructed scalar-coefficient mean is bimodular conditionally only on the indicated published projection theorem.
```
def operatorBimoduleMean (m : ScalarBoundaryMean α)
    (hTom : PublishedFieldTomiyama (G := G) (H := H) (μ := μ)) :
…
```
Mentions: OAI.KadisonKastler.ScalarBoundaryMean, OAI.KadisonKastler.PublishedFieldTomiyama