ConjugateFactor.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Factor transport and composition for a conjugated neighbor

def OAI.KadisonKastler.unitaryConjugateHom line 18
Source documentation
The inner automorphism restricted to the original algebra.
```
def unitaryConjugateHom (w : unitary (H →L[ℂ] H)) (N : VonNeumannAlgebra H) :
    Algebra N →⋆ₐ[ℂ] Algebra (unitaryConjugateAlgebra w N) :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.unitaryConjugateAlgebra
theorem OAI.KadisonKastler.unitaryConjugateHom_apply line 25
theorem OAI.KadisonKastler.unitaryConjugateHom_bijective line 29
def OAI.KadisonKastler.unitaryConjugateEquiv line 41
Source documentation
Exact star-algebra equivalence with the conjugated concrete algebra.
```
def unitaryConjugateEquiv (w : unitary (H →L[ℂ] H)) (N : VonNeumannAlgebra H) :
    Algebra N ≃⋆ₐ[ℂ] Algebra (unitaryConjugateAlgebra w N) :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.unitaryConjugateAlgebra
theorem OAI.KadisonKastler.unitaryConjugateEquiv_apply line 46
theorem OAI.KadisonKastler.unitaryConjugateAlgebra_isII1 line 51
Source documentation
The finite diffuse factor predicate is preserved by unitary conjugation.
```
theorem unitaryConjugateAlgebra_isII1 (w : unitary (H →L[ℂ] H))
    {N : VonNeumannAlgebra H} (hN : Generator.IsII1Factor N.toStarSubalgebra) :
    Generator.IsII1Factor (unitaryConjugateAlgebra w N).toStarSubalgebra :=
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.unitaryConjugateAlgebra
theorem OAI.KadisonKastler.conjugates_of_conjugated_neighbor line 58
Source documentation
Return from the moved neighbor to the original one by composing unitaries.
```
theorem conjugates_of_conjugated_neighbor {M N : VonNeumannAlgebra H}
    (w v : unitary (H →L[ℂ] H))
    (hv : Conjugates v M (unitaryConjugateAlgebra (star w) N)) :
    Conjugates (w * v) M N := by
…
```
Mentions: OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.unitaryConjugateAlgebra

theorem OAI.KadisonKastler.conjugated_neighbor_displacement_le line 67

Source documentation

The final displacement includes the initial movement of the neighbor.

theorem conjugated_neighbor_displacement_le (w v : unitary (H →L[ℂ] H)) :
    ‖((w * v : unitary (H →L[ℂ] H)) : H →L[ℂ] H) - 1‖ ≤
      ‖(w : H →L[ℂ] H) - 1‖ + ‖(v : H →L[ℂ] H) - 1‖ :=
…