ScalarMeanCoefficients.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Matrix coefficients of the scalar boundary mean

A uniformly bounded family of weakly measurable operators gives a sesquilinear family of scalar L-infinity classes. Applying the scalar conditional expectation preserves its algebraic identities and bounds.

structure OAI.KadisonKastler.UniformMeasurableOperators line 27
Source documentation
The exact uniformly bounded measurable family needed for coefficient averaging. The bound is retained as data to control the output operator.
```
structure UniformMeasurableOperators (G D H : Type*) [MeasurableSpace D]
    (μ : Measure D) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] where
…
```
def OAI.KadisonKastler.UniformMeasurableOperators.coefficient line 40
Source documentation
A scalar matrix coefficient is an actual L-infinity class.
```
def coefficient (g : G) (ξ η : H) : ScalarLInfinity μ :=
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
theorem OAI.KadisonKastler.UniformMeasurableOperators.coefficient_ae line 51
theorem OAI.KadisonKastler.UniformMeasurableOperators.norm_coefficient_le line 58
theorem OAI.KadisonKastler.UniformMeasurableOperators.coefficient_add_left line 74
theorem OAI.KadisonKastler.UniformMeasurableOperators.coefficient_smul_left line 83
theorem OAI.KadisonKastler.UniformMeasurableOperators.coefficient_add_right line 92
theorem OAI.KadisonKastler.UniformMeasurableOperators.coefficient_smul_right line 101
def OAI.KadisonKastler.UniformMeasurableOperators.coefficientFamily line 114
Source documentation
All group coordinates of a coefficient form a uniformly bounded family, the precise source space of the scalar mean.
```
def coefficientFamily (ξ η : H) : G →ᵇ ScalarLInfinity μ :=
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
theorem OAI.KadisonKastler.UniformMeasurableOperators.coefficientFamily_apply line 120
theorem OAI.KadisonKastler.UniformMeasurableOperators.norm_coefficientFamily_le line 123
theorem OAI.KadisonKastler.UniformMeasurableOperators.coefficientFamily_add_left line 129
theorem OAI.KadisonKastler.UniformMeasurableOperators.coefficientFamily_smul_left line 135
theorem OAI.KadisonKastler.UniformMeasurableOperators.coefficientFamily_add_right line 141
theorem OAI.KadisonKastler.UniformMeasurableOperators.coefficientFamily_smul_right line 147
def OAI.KadisonKastler.UniformMeasurableOperators.meanCoefficient line 156
Source documentation
Apply the scalar expectation to the actual coefficient family.
```
def meanCoefficient {α : NonsingularAction G D μ} (m : ScalarBoundaryMean α)
    (ξ η : H) : ScalarLInfinity μ := m.toCLM (T.coefficientFamily ξ η)
```
Mentions: OAI.KadisonKastler.NonsingularAction, OAI.KadisonKastler.ScalarBoundaryMean, OAI.KadisonKastler.ScalarLInfinity
theorem OAI.KadisonKastler.UniformMeasurableOperators.norm_meanCoefficient_le line 159
theorem OAI.KadisonKastler.UniformMeasurableOperators.meanCoefficient_add_left line 163
theorem OAI.KadisonKastler.UniformMeasurableOperators.meanCoefficient_smul_left line 168
theorem OAI.KadisonKastler.UniformMeasurableOperators.meanCoefficient_add_right line 172
theorem OAI.KadisonKastler.UniformMeasurableOperators.meanCoefficient_smul_right line 177