PreparedPairCorrection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Preserving the first inclusion under the commutant correction

The second local embedding in the preparation argument is chosen in the von Neumann algebra generated by the right algebra and the neighboring commutant. That entire generated algebra commutes with the common left algebra. These are algebraic consequences of the location of the chosen unitary; its existence is not assumed here as a new perturbation theorem.

theorem OAI.KadisonKastler.generated_right_correction_le_commutant line 25
Source documentation
The right algebra and the neighboring commutant generate an algebra commuting with the common left algebra.
```
theorem generated_right_correction_le_commutant
    (R S N : VonNeumannAlgebra H) (hRN : R ≤ N) (hSR : S ≤ R.commutant) :
    generatedVonNeumannAlgebra (S.toStarSubalgebra ⊔ N.commutant.toStarSubalgebra) ≤
      R.commutant := by
…
```
Mentions: OAI.KadisonKastler.generatedVonNeumannAlgebra
theorem OAI.KadisonKastler.unitaryConj_mem_conjugated_commutant line 38
Source documentation
Membership in a conjugated commutant is the same as conjugating the membership in the original commutant.
```
theorem unitaryConj_mem_conjugated_commutant
    (N : VonNeumannAlgebra H) (w : unitary (H →L[ℂ] H))
    {x : H →L[ℂ] H} (hx : x ∈ N.commutant) :
    unitaryConj w x ∈ (unitaryConjugateAlgebra w N).commutant := by
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.unitaryConjugateAlgebra
theorem OAI.KadisonKastler.right_inclusion_of_moved_right_algebra line 51
Source documentation
Inverse conjugation of a moved right algebra gives the desired right inclusion for the corrected neighboring algebra.
```
theorem right_inclusion_of_moved_right_algebra
    (S N : VonNeumannAlgebra H) (w : unitary (H →L[ℂ] H))
    (hmove : ∀ s ∈ S, unitaryConj w s ∈ N.commutant) :
    S ≤ (unitaryConjugateAlgebra (star w) N).commutant := by
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.unitaryConjugateAlgebra

theorem OAI.KadisonKastler.preparedPair_second_correction line 61

Source documentation

A correction from the indicated generated algebra preserves the first, literal common inclusion and establishes the second one.

theorem preparedPair_second_correction
    (R S N : VonNeumannAlgebra H) (hRN : R ≤ N) (hSR : S ≤ R.commutant)
    (w : unitary (H →L[ℂ] H))
    (hw : (w : H →L[ℂ] H) ∈ generatedVonNeumannAlgebra
      (S.toStarSubalgebra ⊔ N.commutant.toStarSubalgebra))
    (hmove : ∀ s ∈ S, unitaryConj w s ∈ N.commutant) :
    R ≤ unitaryConjugateAlgebra (star w) N ∧
      S ≤ (unitaryConjugateAlgebra (star w) N).commutant := by
…

Mentions: OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.unitaryConjugateAlgebra

theorem OAI.KadisonKastler.preparedPair_second_correction_gap line 78
Source documentation
The corrected pair has the same elementary gap loss as any unitary movement of the neighbor.
```
theorem preparedPair_second_correction_gap
    (M N : VonNeumannAlgebra H) (w : unitary (H →L[ℂ] H)) :
    kkDistance M (unitaryConjugateAlgebra (star w) N) ≤
      kkDistance M N + 2 * ‖(w : H →L[ℂ] H) - 1‖ := by
…
```
Mentions: OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.unitaryConjugateAlgebra