FiniteGroupCorrection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Correcting finite-group unitary representations

The normalized counting mean removes the averaging premise from the bounded quadratic iteration. The constants are independent of the group's order.

theorem OAI.KadisonKastler.exists_finiteGroup_representation line 23

Source documentation

A uniformly approximate finite-group representation is uniformly close to an exact unitary representation in the same C-star algebra.

theorem exists_finiteGroup_representation (V : G → unitary B) {δ : ℝ}
    (hδ : 0 ≤ δ) (hsmall : δ ≤ 1 / 64)
    (hV : ∀ g h, ‖(V g : B) * V h - V (g * h)‖ ≤ δ) :
    ∃ W : G →* unitary B, ∀ g, ‖(W g : B) - V g‖ ≤ 2 * δ := by
…

theorem OAI.KadisonKastler.exists_unitary_finiteGroup_intertwiner line 59

Source documentation

Nearby finite-group representations are conjugate by a near-identity unitary, uniformly in the size of the group.

theorem exists_unitary_finiteGroup_intertwiner (U W : G →* unitary B)
    {δ : ℝ} (hsmall : δ < 1)
    (hclose : ∀ g, ‖(W g : B) - U g‖ ≤ δ) :
    ∃ u : unitary B, (∀ g, (u : B) * U g = (W g : B) * u) ∧
      ‖(u : B) - 1‖ ≤ 2 * δ := by
…