InvariantOperatorMean.lean`

44 declarations, 0 contain sorry, 0 declared as axioms

Operator averaging from an actual scalar invariant mean

The scalar mean is data on bounded scalar functions. Riesz representation constructs the operator average from its coefficients. No operator-valued mean, fixed-point projection, or amenability conclusion is assumed.

def OAI.KadisonKastler.scalarMeanTranslate line 24
structure OAI.KadisonKastler.ScalarInvariantMean line 29
Source documentation
The usual scalar invariant-mean data, with no assertion of existence.
```
structure ScalarInvariantMean (G : Type*) [Group G] [TopologicalSpace G] [DiscreteTopology G] where
…
```
theorem OAI.KadisonKastler.ScalarInvariantMean.fixed line 41
def OAI.KadisonKastler.ScalarInvariantMean.coefficient line 53
Source documentation
The bounded scalar coefficient to which the scalar mean is applied.
```
def coefficient (F : G →ᵇ (H →L[ℂ] H)) (x y : H) : G →ᵇ ℂ :=
…
```
theorem OAI.KadisonKastler.ScalarInvariantMean.coefficient_apply line 64
theorem OAI.KadisonKastler.ScalarInvariantMean.norm_coefficient_le line 68
theorem OAI.KadisonKastler.ScalarInvariantMean.coefficient_add_input line 79
theorem OAI.KadisonKastler.ScalarInvariantMean.coefficient_smul_input line 85
theorem OAI.KadisonKastler.ScalarInvariantMean.coefficient_add_test line 92
theorem OAI.KadisonKastler.ScalarInvariantMean.coefficient_smul_test line 98
def OAI.KadisonKastler.ScalarInvariantMean.testFunctional line 106
Source documentation
A genuine continuous linear scalar functional in the test-vector slot.
```
def testFunctional (F : G →ᵇ (H →L[ℂ] H)) (x : H) : H →L[ℂ] ℂ :=
…
```
def OAI.KadisonKastler.ScalarInvariantMean.operatorValue line 118
theorem OAI.KadisonKastler.ScalarInvariantMean.inner_operatorValue line 121
theorem OAI.KadisonKastler.ScalarInvariantMean.norm_operatorValue_le line 130
def OAI.KadisonKastler.ScalarInvariantMean.operator line 139
theorem OAI.KadisonKastler.ScalarInvariantMean.inner_operator line 155
theorem OAI.KadisonKastler.ScalarInvariantMean.norm_operator_le line 159
theorem OAI.KadisonKastler.ScalarInvariantMean.operator_add line 162
theorem OAI.KadisonKastler.ScalarInvariantMean.operator_smul line 173
def OAI.KadisonKastler.ScalarInvariantMean.operatorMean line 186
Source documentation
The actual contractive complex-linear operator average.
```
def operatorMean : (G →ᵇ (H →L[ℂ] H)) →L[ℂ] (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonKastler.ScalarInvariantMean.inner_operatorMean line 195
theorem OAI.KadisonKastler.ScalarInvariantMean.operatorMean_const line 198
theorem OAI.KadisonKastler.ScalarInvariantMean.operatorMean_left line 208
theorem OAI.KadisonKastler.ScalarInvariantMean.operatorMean_right line 223
theorem OAI.KadisonKastler.ScalarInvariantMean.operatorMean_mem line 232
Source documentation
Averaging an actual family in a von Neumann algebra stays in that algebra.
```
theorem operatorMean_mem (M : VonNeumannAlgebra H) (F : G →ᵇ (H →L[ℂ] H))
    (hF : ∀ g, F g ∈ M) : m.operatorMean F ∈ M := by
…
```
theorem OAI.KadisonKastler.ScalarInvariantMean.operatorMean_isPositive line 243
def OAI.KadisonKastler.ScalarInvariantMean.translateFamily line 261
Source documentation
Translation invariance survives the coefficient construction.
```
def translateFamily (g : G) (F : G →ᵇ (H →L[ℂ] H)) : G →ᵇ (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonKastler.ScalarInvariantMean.operatorMean_translate line 265
def OAI.KadisonKastler.ScalarInvariantMean.evaluationHom line 280
def OAI.KadisonKastler.ScalarInvariantMean.operatorMeanCP line 291
Source documentation
Complete positivity follows by applying scalar positivity to the finite sum of all the matrix coefficients of a positive amplified family.
```
def operatorMeanCP : (G →ᵇ (H →L[ℂ] H)) →CP (H →L[ℂ] H) where
…
```
theorem OAI.KadisonKastler.ScalarInvariantMean.operatorMeanCP_one line 339
def OAI.KadisonKastler.ScalarInvariantMean.conjugationFamily line 343
Source documentation
The orbit family of an operator under an actual unitary representation.
```
def conjugationFamily (U : G →* unitary (H →L[ℂ] H)) (T : H →L[ℂ] H) :
    G →ᵇ (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonKastler.ScalarInvariantMean.conjugationFamily_apply line 348
def OAI.KadisonKastler.ScalarInvariantMean.conjugationFamilyHom line 351
def OAI.KadisonKastler.ScalarInvariantMean.averageConjugation line 380
Source documentation
The unital completely positive invariant average of conjugates.
```
def averageConjugation (U : G →* unitary (H →L[ℂ] H)) :
    (H →L[ℂ] H) →CP (H →L[ℂ] H) where
…
```
theorem OAI.KadisonKastler.ScalarInvariantMean.averageConjugation_apply line 389
theorem OAI.KadisonKastler.ScalarInvariantMean.averageConjugation_one line 392
theorem OAI.KadisonKastler.ScalarInvariantMean.averageConjugation_fixed line 398
theorem OAI.KadisonKastler.ScalarInvariantMean.averageConjugation_invariant line 407

theorem OAI.KadisonKastler.ScalarInvariantMean.averageConjugation_mem line 423

Source documentation

Invariant algebras are preserved by the actual operator average.

theorem averageConjugation_mem (U : G →* unitary (H →L[ℂ] H))
    (M : VonNeumannAlgebra H) (T : H →L[ℂ] H)
    (hT : ∀ g, unitaryConj (U g) T ∈ M) : m.averageConjugation U T ∈ M :=
…

Mentions: OAI.KadisonKastler.unitaryConj

theorem OAI.KadisonKastler.ScalarInvariantMean.averageConjugation_eq_of_commutes line 428

theorem OAI.KadisonKastler.ScalarInvariantMean.norm_averageConjugation_sub_le line 437

Source documentation

A uniform orbit displacement bound is retained by averaging.

theorem norm_averageConjugation_sub_le (U : G →* unitary (H →L[ℂ] H))
    (T : H →L[ℂ] H) {c : ℝ} (hc : 0 ≤ c)
    (hT : ∀ g, ‖unitaryConj (U g) T - T‖ ≤ c) :
    ‖m.averageConjugation U T - T‖ ≤ c := by
…

Mentions: OAI.KadisonKastler.unitaryConj

def OAI.KadisonKastler.ScalarInvariantMean.bimoduleMean line 449
Source documentation
The scalar construction supplies the precise bimodule mean used by the already proved boundary correction.
```
def bimoduleMean : BimoduleMean (boundaryConstant (G := G) (B := H →L[ℂ] H)) where
…
```
Mentions: OAI.KadisonKastler.BimoduleMean, OAI.KadisonKastler.boundaryConstant
theorem OAI.KadisonKastler.ScalarInvariantMean.bimoduleMean_trivial_equivariant line 459
Source documentation
With trivial action on the value algebra, the constructed bimodule mean is equivariant for the actual boundary translation.
```
theorem bimoduleMean_trivial_equivariant (g : G) (F : G →ᵇ (H →L[ℂ] H)) :
    m.bimoduleMean.toCLM
        (boundaryTranslate (1 : G →* ((H →L[ℂ] H) ≃⋆ₐ[ℂ] (H →L[ℂ] H))) g F) =
      m.bimoduleMean.toCLM F := by
…
```
Mentions: OAI.KadisonKastler.boundaryTranslate