FiniteGroupEmbedding.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Moving a finite unitary group into a nearby closed algebra

Correct the unitary approximants inside the target algebra, then average an intertwiner. Both operations have bounds independent of the group's order.

theorem OAI.KadisonKastler.unitary_family_defect_le_of_close line 24

Source documentation

The uniform multiplicative error of a unitary family close to a representation is at most three times the uniform error.

theorem unitary_family_defect_le_of_close (U : G →* unitary A)
    (V : G → unitary A) {e : ℝ} (he : 0 ≤ e)
    (hV : ∀ g, ‖(V g : A) - U g‖ ≤ e) :
    ∀ g h, ‖(V g : A) * V h - V (g * h)‖ ≤ 3 * e := by
…

theorem OAI.KadisonKastler.exists_unitary_finiteGroup_embedding line 46

Source documentation

Uniform unitary approximants in a closed subalgebra give a near-identity unitary moving the whole finite group into that subalgebra.

theorem exists_unitary_finiteGroup_embedding (S : StarSubalgebra ℂ A)
    [IsClosed (S : Set A)] (U : G →* unitary A) (V : G → unitary S)
    {e : ℝ} (he : 0 ≤ e) (hsmall : 3 * e ≤ 1 / 64)
    (hV : ∀ g, ‖(V g : A) - U g‖ ≤ e) :
    ∃ w : unitary A,
      (∀ g, (w : A) * U g * star (w : A) ∈ S) ∧ ‖(w : A) - 1‖ ≤ 14 * e := by
…

theorem OAI.KadisonKastler.exists_unitary_finiteGroup_embedding_of_nearInclusion line 71

Source documentation

The one-sided finite-group embedding supplied by a strict near inclusion.

theorem exists_unitary_finiteGroup_embedding_of_nearInclusion
    {M N : VonNeumannAlgebra H} (U : G →* unitary (Algebra M)) {γ : ℝ}
    (hγ : 0 ≤ γ) (hsmall : γ ≤ 1 / 1152) (hnear : NearInclusion M N γ) :
    ∃ w : unitary (H →L[ℂ] H),
      (∀ g, unitaryConj w (U g : H →L[ℂ] H) ∈ N) ∧
      ‖(w : H →L[ℂ] H) - 1‖ ≤ 84 * γ := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.NearInclusion, OAI.KadisonKastler.unitaryConj