RegularCoreCharacters.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Character multiplication in the regular core representation

The operators Q_a are actual multiplication unitaries on L²(ℝ,H). Their covariance with translations and their commutation with π(B(H)) are proved on representatives. These are the generator identities in the dual-character argument of Section 8.

def OAI.KadisonKastler.regularCharacterScalar line 23
theorem OAI.KadisonKastler.regularCharacterScalar_add_left line 25
theorem OAI.KadisonKastler.regularCharacterScalar_add_right line 30
theorem OAI.KadisonKastler.regularCharacterScalar_continuous line 35
def OAI.KadisonKastler.regularCharacterFiber line 38
theorem OAI.KadisonKastler.regularCharacterFiber_measurable line 51
theorem OAI.KadisonKastler.regularCharacterFiber_star_measurable line 56
def OAI.KadisonKastler.regularCharacterUnitary line 66
Source documentation
The multiplication unitary Q_a ξ(t) = exp(i a t) ξ(t).
```
def regularCharacterUnitary (a : ℝ) :
    unitary (RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularCharacterUnitary_apply_ae line 71
theorem OAI.KadisonKastler.regularCharacterUnitary_zero line 76
theorem OAI.KadisonKastler.regularCharacterUnitary_add line 88
def OAI.KadisonKastler.regularCharacterRepresentation line 106
Source documentation
The actual unitary representation defining the dual-character action.
```
def regularCharacterRepresentation : Multiplicative ℝ →* unitary
    (RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) where
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularCharacter_commute_embedding line 112

theorem OAI.KadisonKastler.regularCharacter_fixes_embedding line 138

Source documentation

The dual characters fix every embedded operator.

theorem regularCharacter_fixes_embedding
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H))
    (hU : ∀ x, Continuous (fun t : ℝ => (U (Multiplicative.ofAdd t) : H →L[ℂ] H) x))
    (a : ℝ) (T : H →L[ℂ] H) :
    unitaryConj (regularCharacterUnitary (H := H) a) (regularCoreEmbedding U hU T) =
…

Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCharacterUnitary, OAI.KadisonKastler.regularCoreEmbedding

theorem OAI.KadisonKastler.regularTranslation_character_covariance line 148
Source documentation
Translation/character covariance, proved directly on L² classes.
```
theorem regularTranslation_character_covariance (a : ℝ) (s : Multiplicative ℝ) :
    (regularRightTranslation (H := H) s : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) *
…
```
Mentions: OAI.KadisonKastler.regularRightTranslation, OAI.KadisonKastler.RegularCoreHilbert