RowReplication.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The diagonal replication of a row and the matrix formula for averaging.

def OAI.KadisonKastler.rowReplication line 16
Source documentation
Place the same row along the diagonal of a rectangular matrix.
```
def rowReplication (r : κ → A) : CStarMatrix ι (ι × κ) A :=
…
```
theorem OAI.KadisonKastler.rowReplication_apply line 20

theorem OAI.KadisonKastler.rowReplication_mul_star line 24

Source documentation

Replicating a normalized row gives a coisometry.

theorem rowReplication_mul_star (r : κ → A) (hr : ∑ k, r k * star (r k) = 1) :
    rowReplication (ι := ι) r * (rowReplication (ι := ι) r).conjTranspose = 1 := by
…

Mentions: OAI.KadisonKastler.rowReplication

theorem OAI.KadisonKastler.mul_rowReplication_apply line 34

Source documentation

Multiplication by the replicated row appends its entries.

theorem mul_rowReplication_apply (X : CStarMatrix τ ι A) (r : κ → A)
    (i : τ) (jk : ι × κ) :
    (X * rowReplication (ι := ι) r : CStarMatrix τ (ι × κ) A) i jk = X i jk.1 * r jk.2 := by
…

Mentions: OAI.KadisonKastler.rowReplication

theorem OAI.KadisonKastler.finiteRightAverage_matrix line 41

Source documentation

The same row average operates at every matrix level.

theorem finiteRightAverage_matrix (r : κ → A) (F : A →ₗ[ℂ] A)
    (X : CStarMatrix τ ι A) :
    CStarMatrix.mapₗ (finiteRightAverage r F) X =
      CStarMatrix.mapₗ F (X * rowReplication r) * (rowReplication r).conjTranspose := by
…

Mentions: OAI.KadisonKastler.finiteRightAverage, OAI.KadisonKastler.rowReplication

theorem OAI.KadisonKastler.rowReplication_norm_bounds line 57

theorem OAI.KadisonKastler.CompletelyBoundedBy.finiteRightAverage line 66

Source documentation

Finite normalized row averages contract the complete norm.

theorem CompletelyBoundedBy.finiteRightAverage {F : A →ₗ[ℂ] A} {c : ℝ}
    (hF : CompletelyBoundedBy F c) (hc : 0 ≤ c)
    (r : κ → A) (hr : ∑ k, r k * star (r k) = 1) :
    CompletelyBoundedBy (finiteRightAverage r F) c := by
…

Mentions: OAI.KadisonKastler.CompletelyBoundedBy