OAI/Analysis/KadisonKastler/CompleteConjugation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The complete displacement of an inner conjugation

  1. def OAI.KadisonKastler.unitaryConjugationLinear line 18

    Source documentation

    Inner conjugation, with its linear-map structure.

    def unitaryConjugationLinear (u : unitary B) : B →ₗ[ℂ] B :=
…
  2. theorem OAI.KadisonKastler.unitaryConjugationLinear_apply line 22
  3. theorem OAI.KadisonKastler.complete_unitaryConjugation_sub_id line 26

    Source documentation

    The same displacement bound holds at every rectangular matrix level.

    theorem complete_unitaryConjugation_sub_id (u : unitary B) :
    CompletelyBoundedBy (unitaryConjugationLinear u - LinearMap.id)
      (2 * ‖(u : B) - 1‖) := by
…

    Mentions: OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.unitaryConjugationLinear