Intertwiner.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Passing an intertwiner to its polar unitary

An invertible intertwiner of star representations has a unitary polar factor which intertwines the same representations. Combining this with the polar estimate gives the near-identity unitary used in the manuscript.

theorem OAI.KadisonKastler.star_intertwines line 22

Source documentation

Taking adjoints reverses the intertwining relation.

theorem star_intertwines (ρ θ : S →⋆ₐ[ℂ] B) {T : B}
    (hT : ∀ x, T * ρ x = θ x * T) (x : S) :
    star T * θ x = ρ x * star T := by
…

theorem OAI.KadisonKastler.intertwiner_star_mul_self_commute line 30
Source documentation
The square of the absolute value of an intertwiner commutes with the source representation.
```
theorem intertwiner_star_mul_self_commute (ρ θ : S →⋆ₐ[ℂ] B) {T : B}
    (hT : ∀ x, T * ρ x = θ x * T) (x : S) :
    Commute (star T * T) (ρ x) := by
…
```
theorem OAI.KadisonKastler.intertwiner_abs_commute line 47
Source documentation
Continuous functional calculus passes the intertwiner commutation relation to its absolute value.
```
theorem intertwiner_abs_commute (ρ θ : S →⋆ₐ[ℂ] B) {T : B}
    (hT : ∀ x, T * ρ x = θ x * T) (x : S) :
    Commute (CFC.abs T) (ρ x) := by
…
```

theorem OAI.KadisonKastler.polar_unitary_intertwines line 54

Source documentation

A unitary factor in the polar decomposition of an invertible intertwiner remains an intertwiner.

theorem polar_unitary_intertwines (ρ θ : S →⋆ₐ[ℂ] B) {T : B}
    (hunit : IsUnit T) (hT : ∀ x, T * ρ x = θ x * T)
    (u : unitary B) (hpolar : (u : B) * CFC.abs T = T) (x : S) :
    (u : B) * ρ x = θ x * (u : B) := by
…

theorem OAI.KadisonKastler.exists_near_unitary_intertwiner line 73

Source documentation

A near-identity star intertwiner produces a near-identity unitary intertwiner. Only the existence of the original intertwiner is assumed.

theorem exists_near_unitary_intertwiner (ρ θ : S →⋆ₐ[ℂ] B) {T : B}
    (hT : ∀ x, T * ρ x = θ x * T) (hnear : ‖T - 1‖ < 1) :
    ∃ u : unitary B, (∀ x, (u : B) * ρ x = θ x * (u : B)) ∧
      ‖(u : B) - 1‖ ≤ 2 * ‖T - 1‖ := by
…

theorem OAI.KadisonKastler.exists_near_unitary_conjugating line 85

Source documentation

Unitary conjugation obtained from a near-identity star intertwiner.

theorem exists_near_unitary_conjugating (ρ θ : S →⋆ₐ[ℂ] B) {T : B}
    (hT : ∀ x, T * ρ x = θ x * T) (hnear : ‖T - 1‖ < 1) :
    ∃ u : unitary B, (∀ x, (u : B) * ρ x * star (u : B) = θ x) ∧
      ‖(u : B) - 1‖ ≤ 2 * ‖T - 1‖ := by
…