KirchbergNumerics.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The scalar cancellation in Kirchberg, J. Operator Theory 36 (1996), page 61. The analytic estimate preceding it is kept separate.

theorem OAI.KadisonSimilarity.log_le_of_kirchberg_inequality line 13
Source documentation
Cancellation of the nonzero K - 1 in Kirchberg's integral estimate.
```
theorem log_le_of_kirchberg_inequality {K D : ℝ} (hK : 1 < K)
    (h : K ≤ 1 + D * ((K - 1) / Real.log K)) : Real.log K ≤ D := by
…
```

theorem OAI.KadisonSimilarity.le_exp_of_kirchberg_inequality line 22

Source documentation

The estimate also covers completely contractive representations.

theorem le_exp_of_kirchberg_inequality {K D : ℝ} (hD : 0 ≤ D)
    (h : 1 < K → K ≤ 1 + D * ((K - 1) / Real.log K)) :
    K ≤ Real.exp D := by
…