AmenableEmbedding.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Moving an injective subalgebra into a nearby algebra

The published input is the one-sided assertion of Cameron--Christensen-- Sinclair--Smith--White--Wiggins, Kadison--Kastler stable factors, Duke Math. J. 163 (2014), Theorem 3.3(i), arXiv:1209.4116v3, p. 13. Only the inclusion and the displacement bound 150 * γ are retained.

theorem OAI.KadisonKastler.nearInclusion_mono_left line 23
Source documentation
Restricting the source preserves a near inclusion with the same bound.
```
theorem nearInclusion_mono_left {R M N : VonNeumannAlgebra H} {γ : ℝ}
    (hRM : R ≤ M) (hMN : NearInclusion M N γ) : NearInclusion R N γ := by
…
```
Mentions: OAI.KadisonKastler.NearInclusion
def OAI.KadisonKastler.PublishedAmenableEmbedding line 30
Source documentation
The one-sided part of CCSSWW Theorem 3.3(i). The location of the unitary in the algebra generated by the two inputs is not needed here.
```
def PublishedAmenableEmbedding : Prop :=
…
```
theorem OAI.KadisonKastler.exists_amenable_embedding_of_kkDistance_lt line 38
Source documentation
A common injective subalgebra of the source can be moved into its nearby neighbor by the published one-sided theorem.
```
theorem exists_amenable_embedding_of_kkDistance_lt
    (hpub : PublishedAmenableEmbedding (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedAmenableEmbedding
theorem OAI.KadisonKastler.centralizer_image_starAlgEquiv line 46
def OAI.KadisonKastler.unitaryConjugateAlgebra line 63
Source documentation
A concrete von Neumann algebra conjugated by an ambient unitary.
```
def unitaryConjugateAlgebra (w : unitary (H →L[ℂ] H)) (M : VonNeumannAlgebra H) :
    VonNeumannAlgebra H where
…
```
theorem OAI.KadisonKastler.conjugates_unitaryConjugateAlgebra line 74
Source documentation
The algebra just constructed is the exact unitary image.
```
theorem conjugates_unitaryConjugateAlgebra (w : unitary (H →L[ℂ] H))
    (M : VonNeumannAlgebra H) : Conjugates w M (unitaryConjugateAlgebra w M) := rfl
```
Mentions: OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.unitaryConjugateAlgebra
theorem OAI.KadisonKastler.le_unitaryConjugateAlgebra_star line 77
theorem OAI.KadisonKastler.exists_common_amenable_neighbor_of_kkDistance_lt line 85
Source documentation
Moving the neighbor back creates a literal common subalgebra. The additional Kadison--Kastler error is at most twice the displacement.
```
theorem exists_common_amenable_neighbor_of_kkDistance_lt
    (hpub : PublishedAmenableEmbedding (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedAmenableEmbedding