InvariantGroupEmbedding.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Near inclusions and groups with an invariant mean

The scalar mean is first restricted to the target von Neumann algebra. Quadratic correction and a single polar intertwiner then embed every member of the represented group simultaneously, including for infinite groups.

theorem OAI.KadisonKastler.exists_group_representation_of_mean line 26
Source documentation
The existing cocycle iteration, specialized to representations and an actual invariant bimodule mean.
```
theorem exists_group_representation_of_mean
    (m : BimoduleMean (boundaryConstant (G := G) (B := B)))
…
```
Mentions: OAI.KadisonKastler.BimoduleMean, OAI.KadisonKastler.boundaryConstant

theorem OAI.KadisonKastler.exists_unitary_invariantGroup_embedding_of_nearInclusion line 65

Source documentation

A single near-identity unitary embeds a group admitting the supplied invariant mean into the neighboring von Neumann algebra.

theorem exists_unitary_invariantGroup_embedding_of_nearInclusion
    (m : ScalarInvariantMean G) {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.ScalarInvariantMean, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.NearInclusion, OAI.KadisonKastler.unitaryConj