UnitaryBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Extending estimates from unitaries

The final step of the uniform amplification argument bounds a linear commutator map on every contraction from its bound on unitaries. This uses the four-unitary decomposition already proved in Mathlib.

theorem OAI.KadisonKastler.norm_le_twice_unitary_bound line 23
Source documentation
A uniform estimate on unitaries extends to the whole algebra with a factor of two. Continuity need not be assumed for this pointwise statement.
```
theorem norm_le_twice_unitary_bound (T : A →ₗ[ℂ] B) {C : ℝ}
    (hT : ∀ u : unitary A, ‖T (u : A)‖ ≤ C) (x : A) :
    ‖T x‖ ≤ 2 * C * ‖x‖ := by
…
```

theorem OAI.KadisonKastler.opNorm_le_twice_unitary_bound line 39

Source documentation

The operator-norm form of the extension from unitaries.

theorem opNorm_le_twice_unitary_bound (T : A →L[ℂ] B) {C : ℝ}
    (hT : ∀ u : unitary A, ‖T (u : A)‖ ≤ C) : ‖T‖ ≤ 2 * C := by
…

theorem OAI.KadisonKastler.norm_le_amplification_bound line 47
Source documentation
The numerical constants used at the end of the manuscript's amplification proof: a unitary bound of 282 δ gives 564 δ.
```
theorem norm_le_amplification_bound (T : A →ₗ[ℂ] B) {δ : ℝ}
    (hT : ∀ u : unitary A, ‖T (u : A)‖ ≤ 282 * δ) (x : A) :
    ‖T x‖ ≤ 564 * δ * ‖x‖ := by
…
```