PairedRepresentations.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Close representations from the published commutant-distance formula

The explicit input PublishedBlockCommutantApproximation is the block specialization of Arveson's distance formula, in the form of Christensen, Perturbations of operator algebras II, Indiana Univ. Math. J. 26 (1977), Proposition 2.1. See also Christensen--Sinclair--Smith--White, Perturbations of C-algebraic invariants*, GAFA 20 (2010), equation (2.1), and Cameron et al., Kadison--Kastler stable factors (2014), equation (2.2).

The 2010 formulation applies to represented C*-algebras. Passing through the quotient by the representation kernel gives the formulation below with the complete bound on the source algebra. No normality is required.

def OAI.KadisonKastler.innerDerivation line 31
Source documentation
The spatial derivation implemented by T.
```
def innerDerivation (T : R) : R →ₗ[ℂ] R :=
…
```
theorem OAI.KadisonKastler.innerDerivation_apply line 35
def OAI.KadisonKastler.pairedRepresentation line 40
Source documentation
The diagonal pair of two star representations.
```
def pairedRepresentation (ρ θ : A →⋆ₐ[ℂ] B) :
    A →⋆ₐ[ℂ] CStarMatrix (Fin 2) (Fin 2) B :=
…
```
theorem OAI.KadisonKastler.pairedRepresentation_apply line 51
theorem OAI.KadisonKastler.innerDerivation_flip_diagonal line 56
theorem OAI.KadisonKastler.pairedRepresentation_commutator_bound line 68
def OAI.KadisonKastler.PublishedBlockCommutantApproximation line 94
Source documentation
The precise strict-approximation consequence of the published commutant-distance formula, restricted to two-by-two operator matrices.
```
def PublishedBlockCommutantApproximation : Prop :=
…
```

theorem OAI.KadisonKastler.close_representations_of_published line 106

Source documentation

Completely close representations are conjugate by a unitary close to the identity, conditional only on the published distance formula.

theorem close_representations_of_published
    (hPublished : PublishedBlockCommutantApproximation A K)
    (ρ θ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) {e : ℝ} (he : 0 ≤ e) (he₁ : e < 1 / 4)
    (hclose : CompletelyBoundedBy (ρ.toAlgHom.toLinearMap - θ.toAlgHom.toLinearMap) e) :
    ∃ u : unitary (K →L[ℂ] K),
      (∀ x, (u : K →L[ℂ] K) * ρ x * star (u : K →L[ℂ] K) = θ x) ∧
      ‖(u : K →L[ℂ] K) - 1‖ ≤ 4 * e := by
…

Mentions: OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.CompletelyBoundedBy