TracialProducts.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Multiplication estimates for the tracial two-norm

theorem OAI.KadisonKastler.traceTwoNorm_mul_le_left line 16
Source documentation
Left multiplication costs at most the ambient operator norm.
```
theorem traceTwoNorm_mul_le_left (τ : FaithfulTracialState B) (x y : B) :
    traceTwoNorm τ (x * y) ≤ ‖x‖ * traceTwoNorm τ y := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.traceTwoNorm_mul_le_right line 50
Source documentation
Right multiplication has the corresponding operator-norm bound.
```
theorem traceTwoNorm_mul_le_right (τ : FaithfulTracialState B) (x y : B) :
    traceTwoNorm τ (x * y) ≤ traceTwoNorm τ x * ‖y‖ := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.traceTwoNorm_unitary_mul line 60
Source documentation
A unitary on the left preserves the tracial two-norm exactly.
```
theorem traceTwoNorm_unitary_mul (τ : FaithfulTracialState B) (u : unitary B) (x : B) :
    traceTwoNorm τ ((u : B) * x) = traceTwoNorm τ x := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.traceTwoNorm_mul_unitary line 72
Source documentation
A unitary on the right preserves the tracial two-norm by traciality.
```
theorem traceTwoNorm_mul_unitary (τ : FaithfulTracialState B) (u : unitary B) (x : B) :
    traceTwoNorm τ (x * (u : B)) = traceTwoNorm τ x := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm