TraceNormPerturbation.lean`

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Trace-norm triangle and sandwich perturbation estimates

theorem OAI.KadisonKastler.trace_re_nonneg line 19
Source documentation
The trace of a positive element is nonnegative.
```
private theorem trace_re_nonneg (τ : FaithfulTracialState B) {a : B} (ha : 0 ≤ a) :
    0 ≤ (τ.toLinearMap a).re := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.traceOneNorm_nonneg line 25
Source documentation
The tracial one-norm is nonnegative.
```
theorem traceOneNorm_nonneg (τ : FaithfulTracialState B) (x : B) :
    0 ≤ traceOneNorm τ x := trace_re_nonneg τ (CFC.abs_nonneg x)
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm, OAI.KadisonKastler.trace_re_nonneg
theorem OAI.KadisonKastler.norm_trace_mul_positive_le line 29
Source documentation
A positive element defines a trace functional bounded by its trace.
```
private theorem norm_trace_mul_positive_le (τ : FaithfulTracialState B)
    (w a : B) (ha : 0 ≤ a) :
    ‖τ.toLinearMap (w * a)‖ ≤ ‖w‖ * (τ.toLinearMap a).re := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
def OAI.KadisonKastler.reconstructionFunction line 48
theorem OAI.KadisonKastler.reconstructionFunction_continuous line 51
theorem OAI.KadisonKastler.reconstructionFunction_bound line 55
def OAI.KadisonKastler.normalizedClip line 76
theorem OAI.KadisonKastler.normalizedClip_norm_le line 78
theorem OAI.KadisonKastler.normalizedClip_reconstruction line 86
theorem OAI.KadisonKastler.norm_trace_mul_le_traceOneNorm line 115
Source documentation
A contraction paired with any element is bounded by its tracial one-norm. Together with approximate duality, this identifies the norm.
```
theorem norm_trace_mul_le_traceOneNorm (τ : FaithfulTracialState B)
    (w x : B) (hw : ‖w‖ ≤ 1) :
    ‖τ.toLinearMap (w * x)‖ ≤ traceOneNorm τ x := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm
theorem OAI.KadisonKastler.traceOneNorm_add_le line 144
Source documentation
Triangle inequality for the tracial one-norm.
```
theorem traceOneNorm_add_le (τ : FaithfulTracialState B) (x y : B) :
    traceOneNorm τ (x + y) ≤ traceOneNorm τ x + traceOneNorm τ y := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm
theorem OAI.KadisonKastler.traceOneNorm_mul_left_le_of_norm_le_one line 157
Source documentation
Left multiplication by a contraction decreases the tracial one-norm.
```
theorem traceOneNorm_mul_left_le_of_norm_le_one (τ : FaithfulTracialState B)
    (a x : B) (ha : ‖a‖ ≤ 1) : traceOneNorm τ (a * x) ≤ traceOneNorm τ x := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm
theorem OAI.KadisonKastler.traceOneNorm_mul_right_le_of_norm_le_one line 172
Source documentation
Right multiplication by a contraction decreases the tracial one-norm.
```
theorem traceOneNorm_mul_right_le_of_norm_le_one (τ : FaithfulTracialState B)
    (x a : B) (ha : ‖a‖ ≤ 1) : traceOneNorm τ (x * a) ≤ traceOneNorm τ x := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm
theorem OAI.KadisonKastler.traceOneNorm_partialIsometry_conjugate line 190
Source documentation
Conjugation by a partial isometry preserves the one-norm of an operator supported on its initial projection.
```
theorem traceOneNorm_partialIsometry_conjugate (τ : FaithfulTracialState B)
    (w x : B) (hw : IsStarProjection (star w * w))
    (hxL : (star w * w) * x = x) (hxR : x * (star w * w) = x) :
    traceOneNorm τ (w * x * star w) = traceOneNorm τ x := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm
theorem OAI.KadisonKastler.traceOneNorm_sandwich_sub_le line 216
Source documentation
Sandwich perturbation, with no selfadjointness requirements on the three elements.
```
theorem traceOneNorm_sandwich_sub_le (τ : FaithfulTracialState B) (s e a : B) :
    traceOneNorm τ (s * a * s - e * a * e) ≤
      traceTwoNorm τ (s - e) * ‖a‖ * (traceTwoNorm τ s + traceTwoNorm τ e) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm, OAI.KadisonKastler.traceTwoNorm