KirchbergConjugation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The entire conjugation path used in Kirchberg's Proposition 1, J. Operator Theory 36 (1996), pp. 60--61.

def OAI.KadisonSimilarity.kirchbergPath line 22
Source documentation
The imaginary direction of this path is unitary conjugation.
```
def kirchbergPath (t a : B) (z : ℂ) : B :=
…
```
theorem OAI.KadisonSimilarity.differentiable_kirchbergPath line 26
theorem OAI.KadisonSimilarity.kirchbergPath_hasDerivAt_zero line 32
theorem OAI.KadisonSimilarity.kirchbergPath_norm_re line 40
theorem OAI.KadisonSimilarity.kirchbergPath_strip_bddAbove line 66
Source documentation
Compactness of the real interval gives boundedness on the infinite strip.
```
theorem kirchbergPath_strip_bddAbove (t a : B) (ht : IsSelfAdjoint t) :
    BddAbove ((norm ∘ kirchbergPath t a) ''
      Complex.HadamardThreeLines.verticalClosedStrip (-1) 1) := by
…
```
Mentions: OAI.KadisonSimilarity.kirchbergPath
theorem OAI.KadisonSimilarity.kirchbergPath_zero line 78

theorem OAI.KadisonSimilarity.kirchbergPath_norm_le line 82

Source documentation

The two boundary bounds control the whole strip, by three lines.

theorem kirchbergPath_norm_le (t a : B) (ht : IsSelfAdjoint t) {M : ℝ}
    (hM : 0 < M) (hleft : ‖kirchbergPath t a (-1)‖ ≤ M)
    (hright : ‖kirchbergPath t a 1‖ ≤ M) {z : ℂ}
    (hz : -1 ≤ z.re ∧ z.re ≤ 1) : ‖kirchbergPath t a z‖ ≤ M := by
…

Mentions: OAI.KadisonSimilarity.kirchbergPath

theorem OAI.KadisonSimilarity.norm_commutator_le_of_kirchberg_bound line 99

Source documentation

Schwarz's lemma gives the scalar derivation bound on page 60.

theorem norm_commutator_le_of_kirchberg_bound (t a : B) (ht : IsSelfAdjoint t)
    {M : ℝ} (hM : 0 < M) (hleft : ‖kirchbergPath t a (-1)‖ ≤ M)
    (hright : ‖kirchbergPath t a 1‖ ≤ M) :
    ‖t * a - a * t‖ ≤ M + ‖a‖ := by
…

Mentions: OAI.KadisonSimilarity.kirchbergPath