TracialCauchySchwarz.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Cauchy–Schwarz for the faithful tracial two-norm

The imaginary-part condition on positive squares gives the Hermitian symmetry of the trace pairing by polarization. The existing algebraic inner-product core then supplies Cauchy–Schwarz, without changing the ambient C*-algebra norm.

theorem OAI.KadisonKastler.FaithfulTracialState.star_pair_symm line 25
Source documentation
Polarization of real positive-square values makes the trace pairing Hermitian.
```
theorem FaithfulTracialState.star_pair_symm (τ : FaithfulTracialState B) (x y : B) :
    star (τ.toLinearMap (star y * x)) = τ.toLinearMap (star x * y) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.FaithfulTracialState.map_star line 40
Source documentation
A positive complex-linear trace commutes with the involution.
```
theorem FaithfulTracialState.map_star (τ : FaithfulTracialState B) (x : B) :
    τ.toLinearMap (star x) = star (τ.toLinearMap x) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
def OAI.KadisonKastler.tracialInnerCore line 45
theorem OAI.KadisonKastler.traceTwoNorm_nonneg line 58
Source documentation
The tracial two-norm is nonnegative.
```
theorem traceTwoNorm_nonneg (τ : FaithfulTracialState B) (x : B) :
    0 ≤ traceTwoNorm τ x := Real.sqrt_nonneg _
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.traceTwoNorm_sq line 62
Source documentation
Its square is the real positive-square trace.
```
theorem traceTwoNorm_sq (τ : FaithfulTracialState B) (x : B) :
    traceTwoNorm τ x ^ 2 = (τ.toLinearMap (star x * x)).re :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.traceTwoNorm_one line 67
theorem OAI.KadisonKastler.traceTwoNorm_star line 71
theorem OAI.KadisonKastler.FaithfulTracialState.cauchySchwarz line 76
Source documentation
Cauchy–Schwarz for the complex trace pairing.
```
theorem FaithfulTracialState.cauchySchwarz (τ : FaithfulTracialState B) (x y : B) :
    ‖τ.toLinearMap (star x * y)‖ ≤ traceTwoNorm τ x * traceTwoNorm τ y := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.FaithfulTracialState.norm_apply_le_traceTwoNorm line 93
Source documentation
Cauchy–Schwarz with the identity bounds a trace by the two-norm.
```
theorem FaithfulTracialState.norm_apply_le_traceTwoNorm (τ : FaithfulTracialState B) (x : B) :
    ‖τ.toLinearMap x‖ ≤ traceTwoNorm τ x := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.traceTwoNorm_add_le line 98
Source documentation
The tracial two-norm satisfies the triangle inequality.
```
theorem traceTwoNorm_add_le (τ : FaithfulTracialState B) (x y : B) :
    traceTwoNorm τ (x + y) ≤ traceTwoNorm τ x + traceTwoNorm τ y := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.traceTwoNorm_le_norm line 119
Source documentation
The tracial two-norm is dominated by the original operator norm.
```
theorem traceTwoNorm_le_norm (τ : FaithfulTracialState B) (x : B) :
    traceTwoNorm τ x ≤ ‖x‖ := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.FaithfulTracialState.norm_apply_le_norm line 137
Source documentation
In particular, the normalized positive trace is a contraction.
```
theorem FaithfulTracialState.norm_apply_le_norm (τ : FaithfulTracialState B) (x : B) :
    ‖τ.toLinearMap x‖ ≤ ‖x‖ :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState