TraceOneNorm.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The product Hölder inequality for the tracial one-norm

def OAI.KadisonKastler.traceOneNorm line 19
Source documentation
The tracial one-norm, using the C*-algebra absolute value.
```
def traceOneNorm (τ : FaithfulTracialState B) (x : B) : ℝ :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
def OAI.KadisonKastler.clippedPolar line 22
def OAI.KadisonKastler.clippedPolarFunction line 24
theorem OAI.KadisonKastler.clippedPolarFunction_continuous line 27
theorem OAI.KadisonKastler.clippedPolarFunction_error line 31
theorem OAI.KadisonKastler.clippedPolar_norm_le line 52
theorem OAI.KadisonKastler.clippedPolar_pair line 60
theorem OAI.KadisonKastler.clippedPolar_pair_error line 84
Source documentation
The clipped polar contraction recovers the absolute value with an operator-norm error at most the cutoff.
```
private theorem clippedPolar_pair_error {ε : ℝ} (hε : 0 < ε) (x : B) :
    ‖CFC.abs x - star (clippedPolar ε x) * x‖ ≤ ε := by
…
```
Mentions: OAI.KadisonKastler.clippedPolar
theorem OAI.KadisonKastler.normalized_spectralClip_norm_le line 100
Source documentation
The explicit normalized spectral clip is a contraction.
```
theorem normalized_spectralClip_norm_le {ε : ℝ} (hε : 0 < ε) (x : B) :
    ‖ε⁻¹ • spectralClip ε x‖ ≤ 1 :=
…
```
Mentions: OAI.KadisonKastler.spectralClip
theorem OAI.KadisonKastler.traceOneNorm_le_normalized_spectralClip_pair line 105
Source documentation
Approximate duality with an explicit continuous cutoff formula.
```
theorem traceOneNorm_le_normalized_spectralClip_pair (τ : FaithfulTracialState B)
    (x : B) {ε : ℝ} (hε : 0 < ε) :
    traceOneNorm τ x ≤
      (τ.toLinearMap (star (ε⁻¹ • spectralClip ε x) * x)).re + ε := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm, OAI.KadisonKastler.spectralClip
theorem OAI.KadisonKastler.traceOneNorm_approx_dual line 117
Source documentation
The tracial one-norm is recovered, to arbitrary accuracy, by pairing with a contraction in the algebra.
```
theorem traceOneNorm_approx_dual (τ : FaithfulTracialState B) (x : B)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ v : B, ‖v‖ ≤ 1 ∧ traceOneNorm τ x ≤
      (τ.toLinearMap (star v * x)).re + ε := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm
theorem OAI.KadisonKastler.traceOneNorm_mul_le line 130
Source documentation
Product Hölder inequality, proved through the clipped polar contractions and Cauchy–Schwarz.
```
theorem traceOneNorm_mul_le (τ : FaithfulTracialState B) (x y : B) :
    traceOneNorm τ (x * y) ≤ traceTwoNorm τ x * traceTwoNorm τ y := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm, OAI.KadisonKastler.traceTwoNorm