CompletelyBoundedRows.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The finite-row consequence of complete boundedness

The definition uses the usual entrywise amplifications on actual C*-matrix algebras. In the properly infinite case, the proved isometry columns turn this definition into precisely the row estimate needed for right averaging.

def OAI.BoundedHochschild.KadisonRingrose.CompletelyBoundedEstimate line 24
Source documentation
A uniform bound on all entrywise matrix amplifications of a linear map.
```
def CompletelyBoundedEstimate (T : M →L[ℂ] M) (C : ℝ) : Prop :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.left_isometry_norm line 28
lemma OAI.BoundedHochschild.KadisonRingrose.columnRow_mul_isometry line 44
lemma OAI.BoundedHochschild.KadisonRingrose.columnCompression_row line 54
theorem OAI.BoundedHochschild.KadisonRingrose.finiteRowBound_of_completelyBounded line 66
Source documentation
Complete boundedness implies the finite-row estimate used by the module projection, via the actual finite matrix amplifications already constructed.
```
theorem finiteRowBound_of_completelyBounded (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hno : NoFiniteCentralSummand M) (T : M →L[ℂ] M) {C : ℝ}
    (hT : CompletelyBoundedEstimate T C) : HasFiniteRowBound T C := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.NoFiniteCentralSummand, OAI.BoundedHochschild.KadisonRingrose.CompletelyBoundedEstimate, OAI.BoundedHochschild.KadisonRingrose.HasFiniteRowBound
theorem OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_norm_of_completelyBounded line 90
Source documentation
The finite elementary averages in the module projection are bounded by any complete bound for the original linear map.
```
theorem finiteRightAverage_norm_of_completelyBounded
    (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (hno : NoFiniteCentralSummand M)
    (m : Fin (n + 1) → M) (hm : ∑ i, m i * star (m i) = 1)
    (T : M →L[ℂ] M) {C : ℝ} (hT : CompletelyBoundedEstimate T C) :
    ‖finiteRightAverage m T‖ ≤ C := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.NoFiniteCentralSummand, OAI.BoundedHochschild.KadisonRingrose.CompletelyBoundedEstimate, OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage