NearInclusionDistance.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.KadisonKastler.exists_unitBall_approx_of_algebra_approx line 17
Source documentation
An algebra approximant can be normalized into its unit ball with at most twice the original error.
```
theorem exists_unitBall_approx_of_algebra_approx
    {x y : H →L[ℂ] H} (hx : ‖x‖ ≤ 1) (hy : y ∈ N) :
    ∃ z ∈ unitBall N, ‖x - z‖ ≤ 2 * ‖x - y‖ := by
…
```
Mentions: OAI.KadisonKastler.unitBall
theorem OAI.KadisonKastler.exists_unitBall_approx_of_nearInclusion line 43
Source documentation
The published strict near-inclusion convention controls the closed unit balls with the factor two from normalization.
```
theorem exists_unitBall_approx_of_nearInclusion {γ : ℝ}
    (h : NearInclusion M N γ) {x : H →L[ℂ] H} (hx : x ∈ unitBall M) :
    ∃ y ∈ unitBall N, ‖x - y‖ < 2 * γ := by
…
```
Mentions: OAI.KadisonKastler.NearInclusion, OAI.KadisonKastler.unitBall
theorem OAI.KadisonKastler.kkDistance_le_two_mul_of_nearInclusions line 53