NormalGNSMatrices.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The faithful normal realization preserves every finite matrix norm. In particular it preserves the complete bounds used in right averaging.

theorem OAI.BoundedHochschild.KadisonRingrose.normalGNS_matrix_norm line 18
Source documentation
Entrywise realization is isometric at each finite matrix size.
```
theorem normalGNS_matrix_norm (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (n : ℕ)
    (A : CStarMatrix (Fin n) (Fin n) M) :
    ‖A.map (normalGNSRepresentation e)‖ = ‖A‖ := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.normalGNSRepresentation
theorem OAI.BoundedHochschild.KadisonRingrose.normalGNS_complete_bound_iff line 28
Source documentation
The concrete Hilbert-space realization has the same complete bound as the original map. No extra regularity of that map is required.
```
theorem normalGNS_complete_bound_iff (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (T : M →L[ℂ] M) (C : ℝ) :
    CompletelyBoundedEstimate T C ↔ 0 ≤ C ∧
      ∀ (n : ℕ) (A : CStarMatrix (Fin n) (Fin n) M),
        ‖(A.map T).map (normalGNSRepresentation e)‖ ≤ C * ‖A‖ := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.CompletelyBoundedEstimate, OAI.BoundedHochschild.KadisonRingrose.normalGNSRepresentation
def OAI.BoundedHochschild.KadisonRingrose.normalGNSLinear line 36
Source documentation
The representation as a continuous linear map.
```
def normalGNSLinear (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
    M →L[ℂ] (NormalGNS e →L[ℂ] NormalGNS e) :=
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.NormalGNS
lemma OAI.BoundedHochschild.KadisonRingrose.normalGNSLinear_apply line 42