OperatorCoefficientMean.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Contractive operator-field averaging from the scalar boundary mean

All objects here are the actual measurable fields modulo almost-everywhere equality. The construction uses norm-minimizing representatives only to produce an operator; its scalar coefficients characterize it intrinsically.

def OAI.KadisonKastler.WeakOperatorField.uniformFamily line 28
Source documentation
Choose norm-controlled representatives of a bounded operator-field family.
```
def uniformFamily (F : G →ᵇ WeakOperatorField (H := H) μ) :
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField
def OAI.KadisonKastler.WeakOperatorField.coefficientFamily line 38
Source documentation
The intrinsic scalar coefficient family.
```
def coefficientFamily (F : G →ᵇ WeakOperatorField (H := H) μ) (ξ η : H) :
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField
theorem OAI.KadisonKastler.WeakOperatorField.coefficientFamily_apply line 42
theorem OAI.KadisonKastler.WeakOperatorField.coefficientFamily_add line 50
theorem OAI.KadisonKastler.WeakOperatorField.coefficientFamily_smul line 57
theorem OAI.KadisonKastler.WeakOperatorField.coefficientFamily_const line 64
def OAI.KadisonKastler.ScalarBoundaryMean.operatorMeanValue line 80
Source documentation
Reconstruct the operator-valued mean from the averaged scalar kernel.
```
def operatorMeanValue (F : G →ᵇ WeakOperatorField (H := H) μ) : WeakOperatorField (H := H) μ :=
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField
theorem OAI.KadisonKastler.ScalarBoundaryMean.operatorMeanValue_coefficient line 84
theorem OAI.KadisonKastler.ScalarBoundaryMean.norm_operatorMeanValue_le line 91
theorem OAI.KadisonKastler.ScalarBoundaryMean.operatorMeanValue_add line 96
theorem OAI.KadisonKastler.ScalarBoundaryMean.operatorMeanValue_smul line 104
def OAI.KadisonKastler.ScalarBoundaryMean.operatorMean line 113
Source documentation
The scalar boundary mean induces a contractive complex-linear map on actual essentially bounded measurable operator fields.
```
def operatorMean : (G →ᵇ WeakOperatorField (H := H) μ) →L[ℂ] WeakOperatorField (H := H) μ :=
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField
theorem OAI.KadisonKastler.ScalarBoundaryMean.operatorMean_apply line 121
theorem OAI.KadisonKastler.ScalarBoundaryMean.operatorMean_fixed line 124