OperatorAlgebra.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Concrete operators for Kadison similarity

These definitions use bounded operators on the actual Hilbert space, and similarity uses a unit of that bounded-operator algebra. The compression estimate is the operator calculation in Lemma lem:compressed-commutator of the manuscript.

abbrev OAI.KadisonSimilarity.BoundedUnitalHom line 25
Source documentation
A complex-linear unital algebra homomorphism which is bounded.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:16 (same declaration text).
```
abbrev BoundedUnitalHom :=
…
```
def OAI.KadisonSimilarity.SimilarToStar line 29
Source documentation
Similarity by a bounded invertible operator to an adjoint-preserving homomorphism.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:19 (same declaration text).
```
def SimilarToStar (π : BoundedUnitalHom A H) : Prop :=
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom
theorem OAI.KadisonSimilarity.similarToStar_of_star line 35
Source documentation
An already adjoint-preserving homomorphism requires no change of coordinates.
```
theorem similarToStar_of_star (π : BoundedUnitalHom A H)
    (hπ : ∀ a : A, π.1 (star a) = star (π.1 a)) : SimilarToStar A H π := by
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.SimilarToStar
theorem OAI.KadisonSimilarity.similarToStar_metric line 43
Source documentation
The positive metric identity attached to a similarity. This is the algebraic identity used in the completely bounded implementation argument.
```
theorem similarToStar_metric (π : BoundedUnitalHom A H) :
    SimilarToStar A H π ↔
      ∃ S : (H →L[ℂ] H)ˣ, ∀ a : A,
        (star (S : H →L[ℂ] H) * (S : H →L[ℂ] H)) * π.1 (star a) =
          star (π.1 a) * (star (S : H →L[ℂ] H) * (S : H →L[ℂ] H)) := by
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.SimilarToStar
def OAI.KadisonSimilarity.commutator line 73
Source documentation
The commutator, with the sign convention of the manuscript.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:30 (same declaration text).
```
def commutator (S T : R) : R := S * T - T * S
```
theorem OAI.KadisonSimilarity.commutator_zero_left line 75
theorem OAI.KadisonSimilarity.commutator_zero_right line 78
theorem OAI.KadisonSimilarity.commutator_sub_left line 81
theorem OAI.KadisonSimilarity.norm_commutator_le line 87
Source documentation
Replacing an operator changes a commutator by at most twice its norm change.
```
theorem norm_commutator_le (S T : R) :
    ‖commutator S T‖ ≤ 2 * ‖S‖ * ‖T‖ := by
…
```
Mentions: OAI.KadisonSimilarity.commutator
theorem OAI.KadisonSimilarity.norm_commutator_sub_le line 94
theorem OAI.KadisonSimilarity.norm_commutator_le_of_approx line 100
Source documentation
The perturbation estimate used when restoring the original operator after averaging.
```
theorem norm_commutator_le_of_approx (S T U : R) {a d : ℝ}
    (hT : ‖commutator T U‖ ≤ a) (hST : ‖S - T‖ ≤ d) :
    ‖commutator S U‖ ≤ a + 2 * d * ‖U‖ := by
…
```
Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.compression_commutator_identity line 120

Source documentation

Exact compression identity, including both full-codomain errors.

theorem compression_commutator_identity (G T : H →L[ℂ] H)
    (J : K →L[ℂ] K) (ι : K →L[ℂ] H) :
    commutator J (ι.adjoint.comp (T.comp ι)) =
      ι.adjoint.comp ((commutator G T).comp ι) -
        (G.adjoint.comp ι - ι.comp J.adjoint).adjoint.comp (T.comp ι) +
        ι.adjoint.comp (T.comp (G.comp ι - ι.comp J)) := by
…

Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.norm_compressed_commutator_le line 132

Source documentation

Lemma lem:compressed-commutator: a contractive inclusion transfers a commutator estimate, with one contribution from each intertwining error.

theorem norm_compressed_commutator_le (G T : H →L[ℂ] H)
    (J : K →L[ℂ] K) (ι : K →L[ℂ] H) {ε η : ℝ}
    (hι : ‖ι‖ ≤ 1)
    (hG : ‖commutator G T‖ ≤ ε * ‖T‖)
    (hR : ‖G.comp ι - ι.comp J‖ ≤ η)
    (hR' : ‖G.adjoint.comp ι - ι.comp J.adjoint‖ ≤ η) :
    ‖commutator J (ι.adjoint.comp (T.comp ι))‖ ≤ (ε + 2 * η) * ‖T‖ := by
…

Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.norm_compressed_commutator_le_paper line 179

Source documentation

The manuscript's constant after the two propagation errors are substituted.

theorem norm_compressed_commutator_le_paper (G T : H →L[ℂ] H)
    (J : K →L[ℂ] K) (ι : K →L[ℂ] H) {ε c₀ : ℝ}
    (hι : ‖ι‖ ≤ 1)
    (hG : ‖commutator G T‖ ≤ ε * ‖T‖)
    (hR : ‖G.comp ι - ι.comp J‖ ≤ 2 * c₀ * ε)
    (hR' : ‖G.adjoint.comp ι - ι.comp J.adjoint‖ ≤ 2 * c₀ * ε) :
    ‖commutator J (ι.adjoint.comp (T.comp ι))‖ ≤ (1 + 4 * c₀) * ε * ‖T‖ := by
…

Mentions: OAI.KadisonSimilarity.commutator