CharacterAverageDescent.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Descent by the character-action average

The concrete crossed-product representation identifies the joint fixed algebra with the embedded original algebra. Once that actual identity is available, the scalar character mean supplies the UCP map required for descent. No statement that its entire ambient range is embedded is used.

theorem OAI.KadisonKastler.mem_jointFixedPointAlgebra_iff line 25

theorem OAI.KadisonKastler.fixedPointAlgebra_interchange line 34

Source documentation

Joint fixed points do not depend on the order of the two conditions.

theorem fixedPointAlgebra_interchange
    (U : G →* unitary (K →L[ℂ] K)) (V : L →* unitary (K →L[ℂ] K))
    (B : VonNeumannAlgebra K) :
    fixedPointAlgebra V (fixedPointAlgebra U B) =
      fixedPointAlgebra U (fixedPointAlgebra V B) := by
…

Mentions: OAI.KadisonKastler.fixedPointAlgebra

theorem OAI.KadisonKastler.normalizes_fixedPointAlgebra_of_commuting_actions line 44

Source documentation

Commuting conjugation actions restrict to each other's fixed algebra.

theorem normalizes_fixedPointAlgebra_of_commuting_actions
    (U : G →* unitary (K →L[ℂ] K)) (V : L →* unitary (K →L[ℂ] K))
    (B : VonNeumannAlgebra K)
    (hB : ∀ l T, T ∈ B → unitaryConj (V l) T ∈ B)
    (hcomm : ∀ g l T, unitaryConj (U g) (unitaryConj (V l) T) =
      unitaryConj (V l) (unitaryConj (U g) T)) :
    ∀ l T, T ∈ fixedPointAlgebra U B →
      unitaryConj (V l) T ∈ fixedPointAlgebra U B := by
…

Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.fixedPointAlgebra

def OAI.KadisonKastler.characterAverage line 84
Source documentation
The same proved average, expressed with the spectral-order instances used by the descent criterion. Its matrix positivity is unchanged.
```
def characterAverage (m : ScalarInvariantMean L) (V : L →* unitary (K →L[ℂ] K)) :
    (K →L[ℂ] K) →CP (K →L[ℂ] K) where
…
```
Mentions: OAI.KadisonKastler.ScalarInvariantMean

theorem OAI.KadisonKastler.characterAverage_conjugate_mem_range line 97

Source documentation

The character average has the exact range property needed on the conjugated source. Only the joint fixed algebra is identified with j(N).

theorem characterAverage_conjugate_mem_range
    (m : ScalarInvariantMean L)
    (U : G →* unitary (K →L[ℂ] K)) (V : L →* unitary (K →L[ℂ] K))
    (A B : VonNeumannAlgebra K)
    (j : (H →L[ℂ] H) →⋆ₐ[ℂ] (K →L[ℂ] K))
    (hV : ∀ l T, T ∈ fixedPointAlgebra U B →
      unitaryConj (V l) T ∈ fixedPointAlgebra U B)
    (hjoint : (fixedPointAlgebra V (fixedPointAlgebra U B) : Set (K →L[ℂ] K)) =
      j '' (N : Set (H →L[ℂ] H)))
    (hjM : ∀ x : Algebra M, j x ∈ fixedPointAlgebra U A)
    (z : unitary (K →L[ℂ] K))
    (hz : Conjugates z (fixedPointAlgebra U A) (fixedPointAlgebra U B))
…

Mentions: OAI.KadisonKastler.ScalarInvariantMean, OAI.KadisonKastler.fixedPointAlgebra, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.Conjugates

theorem OAI.KadisonKastler.concrete_unitary_of_character_average line 121

Source documentation

A conjugacy of the first fixed algebras descends through the actual character average to a nearby unitary on the original Hilbert space.

theorem concrete_unitary_of_character_average
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (m : ScalarInvariantMean L)
    (U : G →* unitary (K →L[ℂ] K)) (V : L →* unitary (K →L[ℂ] K))
    (A B : VonNeumannAlgebra K)
    (j : (H →L[ℂ] H) →⋆ₐ[ℂ] (K →L[ℂ] K)) (hj : Function.Injective j)
    (hV : ∀ l T, T ∈ fixedPointAlgebra U B →
      unitaryConj (V l) T ∈ fixedPointAlgebra U B)
    (hjoint : (fixedPointAlgebra V (fixedPointAlgebra U B) : Set (K →L[ℂ] K)) =
      j '' (N : Set (H →L[ℂ] H)))
    (hjM : ∀ x : Algebra M, j x ∈ fixedPointAlgebra U A)
…

Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ScalarInvariantMean, OAI.KadisonKastler.fixedPointAlgebra, OAI.KadisonKastler.unitaryConj