RegularCoreActions.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Normalization by the two actual regular actions

The translation and character formulas imply the required tensor-algebra normalization. The two actions commute as conjugations, although their implementing unitary groups commute only up to scalar characters.

theorem OAI.KadisonKastler.commute_conjugated_of_conjugate_commute line 22
theorem OAI.KadisonKastler.unitaryConj_star_eq_of_commute line 35
theorem OAI.KadisonKastler.regularCharacter_commute_constant line 43
Source documentation
Constant operators commute with the actual scalar character multipliers.
```
theorem regularCharacter_commute_constant (a : ℝ) (T : H →L[ℂ] H) :
    Commute (regularCharacterUnitary (H := H) a :
…
```
Mentions: OAI.KadisonKastler.regularCharacterUnitary
theorem OAI.KadisonKastler.tensor_mem_conjugate_of_constant_commute line 62
theorem OAI.KadisonKastler.regularTranslation_normalizes_tensor line 76
Source documentation
Translation preserves the tensor algebra, without any action on P.
```
theorem regularTranslation_normalizes_tensor (P : VonNeumannAlgebra H)
    (s : Multiplicative ℝ) {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hT : T ∈ regularTensorAlgebra P) :
    unitaryConj (regularRightTranslation (H := H) s) T ∈ regularTensorAlgebra P :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularTensorAlgebra, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularRightTranslation
theorem OAI.KadisonKastler.regularCharacter_normalizes_tensor line 84
Source documentation
Scalar characters preserve the tensor algebra.
```
theorem regularCharacter_normalizes_tensor (P : VonNeumannAlgebra H)
    (a : Multiplicative ℝ) {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hT : T ∈ regularTensorAlgebra P) :
    unitaryConj (regularCharacterRepresentation (H := H) a) T ∈ regularTensorAlgebra P :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularTensorAlgebra, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCharacterRepresentation
theorem OAI.KadisonKastler.regularConstant_conjugation line 91
theorem OAI.KadisonKastler.conjugate_commutant_of_normalizes line 100
theorem OAI.KadisonKastler.regularConstant_normalizes_tensor line 111

theorem OAI.KadisonKastler.regularCoreAction_normalizes_tensor line 127

Source documentation

The common regular action preserves the tensor algebra whenever the original group normalizes P.

theorem regularCoreAction_normalizes_tensor
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H)) (P : VonNeumannAlgebra H)
    (hP : ∀ s x, x ∈ P → unitaryConj (U s) x ∈ P)
    (s : Multiplicative ℝ) {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hT : T ∈ regularTensorAlgebra P) :
    unitaryConj (regularCoreAction U s) T ∈ regularTensorAlgebra P := by
…

Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularTensorAlgebra, OAI.KadisonKastler.regularCoreAction

theorem OAI.KadisonKastler.conjugations_commute_of_scalar_product line 139
theorem OAI.KadisonKastler.regularCore_character_actions_commute line 153
Source documentation
The regular and character actions commute as inner automorphisms.
```
theorem regularCore_character_actions_commute
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H)) (s a : Multiplicative ℝ)
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) :
    unitaryConj (regularCoreAction U s)
        (unitaryConj (regularCharacterRepresentation (H := H) a) T) =
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCoreAction, OAI.KadisonKastler.regularCharacterRepresentation
theorem OAI.KadisonKastler.regularCharacter_normalizes_coreFixed line 189
Source documentation
The dual character action preserves the actual core fixed algebra.
```
theorem regularCharacter_normalizes_coreFixed
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H)) (P : VonNeumannAlgebra H)
    (a : Multiplicative ℝ) {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hT : T ∈ fixedPointAlgebra (regularCoreAction U) (regularTensorAlgebra P)) :
    unitaryConj (regularCharacterRepresentation (H := H) a) T ∈
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.fixedPointAlgebra, OAI.KadisonKastler.regularCoreAction, OAI.KadisonKastler.regularTensorAlgebra, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCharacterRepresentation

theorem OAI.KadisonKastler.regular_jointFixed_coe line 202

Source documentation

Set form of the joint fixed-point identity, matching the range premise of the character-average descent theorem.

theorem regular_jointFixed_coe
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H))
    (hU : ∀ ξ, Continuous (fun t : ℝ => (U (Multiplicative.ofAdd t) : H →L[ℂ] H) ξ))
    [TopologicalSpace.SeparableSpace H]
    (hSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u})
    (P : VonNeumannAlgebra H)
    (hP : ∀ s x, x ∈ P → unitaryConj (U s) x ∈ P) :
    (fixedPointAlgebra (regularCharacterRepresentation (H := H))
…

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