UnitaryApproximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Unitary approximants in a nearby finite factor

The finite-factor polar decomposition turns contraction approximants into unitary approximants with three times the error. This supplies the actual initial unitary family for boundary correction.

theorem OAI.KadisonKastler.exists_unitary_near_of_II1 line 26

Source documentation

Polar normalization of a contraction approximant costs a factor of three.

theorem exists_unitary_near_of_II1
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    (u : unitary (H →L[ℂ] H)) (x : Algebra N) (hx : ‖x‖ ≤ 1) :
    ∃ v : unitary (Algebra N),
      ‖(v : H →L[ℂ] H) - (u : H →L[ℂ] H)‖ ≤
        3 * ‖(x : H →L[ℂ] H) - (u : H →L[ℂ] H)‖ := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_unitary_approx_of_kkDistance line 47

Source documentation

Every unitary of the first algebra has a nearby unitary in the neighboring finite factor.

theorem exists_unitary_approx_of_kkDistance
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    {b : ℝ} (hgap : kkDistance M N < b) (u : unitary (Algebra M)) :
    ∃ v : unitary (Algebra N),
      ‖(v : H →L[ℂ] H) - (u : H →L[ℂ] H)‖ < 3 * b := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.unitary_family_multiplicative_defect line 63

Source documentation

A family uniformly close to a unitary representation has multiplicative defect at most three times its approximation error.

theorem unitary_family_multiplicative_defect
    {G : Type*} [Group G] (U : G →* unitary (H →L[ℂ] H))
    (V : G → unitary (H →L[ℂ] H)) {e : ℝ}
    (hV : ∀ g, ‖(V g : H →L[ℂ] H) - (U g : H →L[ℂ] H)‖ ≤ e)
    (g h : G) :
    ‖(V g : H →L[ℂ] H) * V h - V (g * h)‖ ≤ 3 * e := by
…