FiniteRightAveraging.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Elementary right averages of bounded linear maps

These are the finite averages used in the completely bounded module-map projection. The norm estimate only uses the precise finite-row inequality.

def OAI.BoundedHochschild.KadisonRingrose.HasFiniteRowBound line 20
Source documentation
A finite-row bound, expressed in the C*-algebra without an auxiliary operator-space structure.
```
def HasFiniteRowBound (T : M →L[ℂ] M) (C : ℝ) : Prop :=
…
```
def OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage line 27
Source documentation
The elementary average x ↦ ∑ T(x mᵢ) mᵢ*.
```
def finiteRightAverage (m : I → M) (T : M →L[ℂ] M) : M →L[ℂ] M :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_apply line 31
lemma OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_add line 36
lemma OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_smul line 41
lemma OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_leftOutput line 47
lemma OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_precompose_left line 54
lemma OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_mul_left line 61

theorem OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_norm_of_rowBound line 76

Source documentation

Finite normalized right averages satisfy the row norm bound.

theorem finiteRightAverage_norm_of_rowBound
    (c : Fin n → HochschildComparison.PartialIso M)
    (hi : ∀ i, (c i).initial = 1)
    (ho : ∀ i j, i ≠ j → (c i).final * (c j).final = 0)
    (m : Fin n → M) (hm : ∑ i, m i * star (m i) = 1)
    (T : M →L[ℂ] M) {C : ℝ} (hT : HasFiniteRowBound T C) :
    ‖finiteRightAverage m T‖ ≤ C := by
…

Mentions: OAI.HochschildComparison.PartialIso, OAI.BoundedHochschild.KadisonRingrose.HasFiniteRowBound, OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage