CommonPositionTransfer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Returning a common-position isomorphism to the original space

def OAI.KadisonKastler.CommonTracialPositionData.transportEquiv line 23
Source documentation
Transport through the two faithful representations.
```
def transportEquiv (θ : Algebra d.left ≃⋆ₐ[ℂ] Algebra d.right) :
    Algebra M ≃⋆ₐ[ℂ] Algebra N :=
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.CommonTracialPositionData.rightEquiv_transportEquiv line 28

theorem OAI.KadisonKastler.CommonTracialPositionData.transportEquiv_unitBall_bound line 35

Source documentation

The comparison of original contractions in the published theorem is exactly what transfers the perturbation estimate back to the original Hilbert space.

theorem transportEquiv_unitBall_bound
    (θ : Algebra d.left ≃⋆ₐ[ℂ] Algebra d.right) {C : ℝ} (hC : 0 ≤ C)
    (hθ : ∀ x : Algebra d.left,
      ‖(θ x : K →L[ℂ] K) - (x : K →L[ℂ] K)‖ ≤ C * ‖x‖)
    (hgap : kkDistance M N < g) (x : Algebra M) (hx : ‖x‖ ≤ 1) :
    ‖(d.transportEquiv θ x : H →L[ℂ] H) - (x : H →L[ℂ] H)‖ ≤
      C + d.tolerance + 2 * g := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.kkDistance

theorem OAI.KadisonKastler.CommonTracialPositionData.transportEquiv_bound line 72

Source documentation

The transferred estimate holds on every algebra element, with no loss in its constant.

theorem transportEquiv_bound
    (θ : Algebra d.left ≃⋆ₐ[ℂ] Algebra d.right) {C : ℝ} (hC : 0 ≤ C)
    (hθ : ∀ x : Algebra d.left,
      ‖(θ x : K →L[ℂ] K) - (x : K →L[ℂ] K)‖ ≤ C * ‖x‖)
    (hgap : kkDistance M N < g) (x : Algebra M) :
    ‖(d.transportEquiv θ x : H →L[ℂ] H) - (x : H →L[ℂ] H)‖ ≤
      (C + d.tolerance + 2 * g) * ‖x‖ := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.kkDistance