UnitaryExtension.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Extending the unitary commutator estimate to the whole algebra

theorem OAI.KadisonKastler.linear_norm_le_twice_unitary_bound line 19
Source documentation
The four-unitary decomposition loses only a factor of two when extending a linear norm estimate from unitaries to arbitrary elements.
```
theorem linear_norm_le_twice_unitary_bound (F : A →ₗ[ℂ] V) {C : ℝ}
    (hF : ∀ u : unitary A, ‖F (u : A)‖ ≤ C) (x : A) :
    ‖F x‖ ≤ 2 * C * ‖x‖ := by
…
```

theorem OAI.KadisonKastler.linear_norm_le_five_sixty_four line 34

Source documentation

The numerical final step of the amplification argument.

theorem linear_norm_le_five_sixty_four (F : A →ₗ[ℂ] V) {δ : ℝ}
    (hF : ∀ u : unitary A, ‖F (u : A)‖ ≤ 282 * δ) (x : A) :
    ‖F x‖ ≤ 564 * δ * ‖x‖ := by
…

theorem OAI.KadisonKastler.linear_norm_le_six_hundred line 42

Source documentation

The manuscript uses the round universal constant 600.

theorem linear_norm_le_six_hundred (F : A →ₗ[ℂ] V) {δ : ℝ}
    (hδ : 0 ≤ δ) (hF : ∀ u : unitary A, ‖F (u : A)‖ ≤ 282 * δ) (x : A) :
    ‖F x‖ ≤ 600 * δ * ‖x‖ := by
…