OAI/Analysis/KadisonKastler/ContinuousPolarPath.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Continuous polar unitary paths

The polar decomposition identifies its unitary factor with a * inverse(abs a). This gives norm continuity for continuous paths of invertible operators, together with quantitative smoothing bounds.

  1. def OAI.KadisonKastler.polarUnitary line 20
  2. theorem OAI.KadisonKastler.polarUnitary_mul_abs line 22
  3. theorem OAI.KadisonKastler.polarUnitary_eq_mul_inverse_abs line 26
  4. theorem OAI.KadisonKastler.polarUnitary_unique line 36
  5. theorem OAI.KadisonKastler.continuous_polarUnitary line 46
  6. theorem OAI.KadisonKastler.continuous_polarUnitary_of_isUnit line 66

    Source documentation

    A continuous operator family known pointwise to be invertible gives an actual norm-continuous family of polar unitaries.

    theorem continuous_polarUnitary_of_isUnit {X : Type*} [TopologicalSpace X]
    (f : X → A) (hf : Continuous f) (hunit : ∀ x, IsUnit (f x)) :
    Continuous (fun x => polarUnitary (hunit x).unit) := by
…

    Mentions: OAI.KadisonKastler.polarUnitary

  7. theorem OAI.KadisonKastler.norm_polarUnitary_sub_le line 76