OAI/Analysis/KadisonKastler/ExponentialCommutator.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exponentiating a bounded inner derivation

  1. def OAI.KadisonKastler.boundedCommutator line 15

    Source documentation

    The bounded commutator operator on a normed algebra.

    def boundedCommutator (x : A) : A →L[ℂ] A :=
…
  2. theorem OAI.KadisonKastler.boundedCommutator_apply line 19
  3. theorem OAI.KadisonKastler.norm_boundedCommutator_le line 23
  4. theorem OAI.KadisonKastler.leftMul_pow_apply line 33
  5. theorem OAI.KadisonKastler.rightMul_pow_apply line 43
  6. theorem OAI.KadisonKastler.exp_leftMul_apply line 52
  7. theorem OAI.KadisonKastler.exp_rightMul_apply line 66
  8. theorem OAI.KadisonKastler.exp_boundedCommutator_apply line 81

    Source documentation

    The identity holds in every complete complex normed algebra.

    theorem exp_boundedCommutator_apply (x y : A) :
    NormedSpace.exp (boundedCommutator x) y =
      NormedSpace.exp x * y * NormedSpace.exp (-x) := by
…

    Mentions: OAI.KadisonKastler.boundedCommutator