FixedPointGap.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Fixed-point algebras and the common-action gap

The fixed algebra is an actual von Neumann algebra, defined as a commutant. The scalar invariant mean constructed in InvariantOperatorMean averages ordinary unit-ball approximants into fixed-point approximants without increasing either their norm or their error. No existence of a scalar mean or fixed-point averaging map is postulated here.

def OAI.KadisonKastler.fixedPointAlgebra line 25
Source documentation
Fixed points inside M, expressed as the commutant of M' together with the given representation.
```
def fixedPointAlgebra (U : G →* unitary (H →L[ℂ] H))
    (M : VonNeumannAlgebra H) : VonNeumannAlgebra H where
…
```
theorem OAI.KadisonKastler.mem_fixedPointAlgebra_iff line 36
theorem OAI.KadisonKastler.fixedPointAlgebra_le line 62
theorem OAI.KadisonKastler.ScalarInvariantMean.averageConjugation_mem_fixed line 72
Source documentation
Actual averaging takes invariant-algebra elements to its fixed algebra.
```
theorem averageConjugation_mem_fixed (M : VonNeumannAlgebra H)
    (hM : ∀ g T, T ∈ M → unitaryConj (U g) T ∈ M)
    {T : H →L[ℂ] H} (hT : T ∈ M) :
    m.averageConjugation U T ∈ fixedPointAlgebra U M := by
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.fixedPointAlgebra
theorem OAI.KadisonKastler.ScalarInvariantMean.averageConjugation_fixed_on_fixed line 80
theorem OAI.KadisonKastler.ScalarInvariantMean.averageConjugation_norm_le line 85
theorem OAI.KadisonKastler.ScalarInvariantMean.exists_fixedPoint_unitBall_approx line 90
theorem OAI.KadisonKastler.ScalarInvariantMean.kkDistance_fixedPointAlgebra_le line 112
Source documentation
A common unitary action cannot increase the ordinary Kadison--Kastler gap upon passage to fixed points.
```
theorem kkDistance_fixedPointAlgebra_le
    (M N : VonNeumannAlgebra H)
    (hM : ∀ g T, T ∈ M → unitaryConj (U g) T ∈ M)
    (hN : ∀ g T, T ∈ N → unitaryConj (U g) T ∈ N) :
    kkDistance (fixedPointAlgebra U M) (fixedPointAlgebra U N) ≤ kkDistance M N := by
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.fixedPointAlgebra