RegularCoreRepresentation.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

The real regular representation and the core embedding

The translation and gauge operators below act on L²(ℝ,H) itself. A strongly continuous unitary group gives the faithful embedding π(x)(t) = U(t)* x U(t). No crossed-product or fixed-point identification is assumed in these constructions.

def OAI.KadisonKastler.regularTranslateApply line 25
Source documentation
Right translation of actual L² classes.
```
def regularTranslateApply (s : ℝ) (f : RegularCoreHilbert H) : RegularCoreHilbert H :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularTranslateApply_ae line 29
theorem OAI.KadisonKastler.regularTranslateApply_add line 34
theorem OAI.KadisonKastler.regularTranslateApply_zero line 45
def OAI.KadisonKastler.regularTranslationEquiv line 51
def OAI.KadisonKastler.regularRightTranslation line 63
Source documentation
The concrete right-translation unitary ρ_s ξ(t)=ξ(t+s).
```
def regularRightTranslation : Multiplicative ℝ →* unitary
    (RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) where
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularRightTranslation_apply_ae line 80
theorem OAI.KadisonKastler.regularConstant_commute_translation line 86
Source documentation
Constant operators commute with translations.
```
theorem regularConstant_commute_translation (T : H →L[ℂ] H) (s : Multiplicative ℝ) :
    Commute (regularConstantHom volume T)
      (regularRightTranslation (H := H) s : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) := by
…
```
Mentions: OAI.KadisonKastler.regularConstantHom, OAI.KadisonKastler.regularRightTranslation, OAI.KadisonKastler.RegularCoreHilbert
def OAI.KadisonKastler.regularConstantUnitary line 110
Source documentation
The constant copy of a unitary as an actual unitary on L².
```
def regularConstantUnitary : unitary (H →L[ℂ] H) →* unitary
    (RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularGroup_star_eq line 117
theorem OAI.KadisonKastler.regularGroup_star_measurable line 123
def OAI.KadisonKastler.regularGauge line 135
Source documentation
Multiplication by U_t, as a unitary on the regular Hilbert space.
```
def regularGauge : unitary (RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularGauge_apply_ae line 139
theorem OAI.KadisonKastler.regularGauge_star_apply_ae line 144
def OAI.KadisonKastler.regularCoreEmbedding line 171
Source documentation
The regular embedding π(x) = gauge* · constant(x) · gauge.
```
def regularCoreEmbedding : (H →L[ℂ] H) →⋆ₐ[ℂ]
    (RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularCoreEmbedding_apply_ae line 176
theorem OAI.KadisonKastler.regularCoreEmbedding_injective line 194
theorem OAI.KadisonKastler.regularCoreEmbedding_completelyIsometric line 198
def OAI.KadisonKastler.regularCoreAction line 203
Source documentation
The common regular action U_s ⊗ ρ_s, without any fixed-point premise.
```
def regularCoreAction : Multiplicative ℝ →* unitary
    (RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) where
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularCoreAction_apply_ae line 223
theorem OAI.KadisonKastler.regularGauge_intertwines_action line 234
Source documentation
The gauge turns the common regular action into ordinary translation.
```
theorem regularGauge_intertwines_action (s : Multiplicative ℝ) :
    (regularGauge U hU : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) *
        regularCoreAction U s =
      (regularRightTranslation (H := H) s : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) *
…
```
Mentions: OAI.KadisonKastler.regularGauge, OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularCoreAction, OAI.KadisonKastler.regularRightTranslation
theorem OAI.KadisonKastler.regularCoreAction_eq_gauged_translation line 259
theorem OAI.KadisonKastler.regularCoreEmbedding_fixed line 272
Source documentation
Every embedded operator is fixed by the common regular action.
```
theorem regularCoreEmbedding_fixed (s : Multiplicative ℝ) (T : H →L[ℂ] H) :
    unitaryConj (regularCoreAction U s) (regularCoreEmbedding U hU T) =
      regularCoreEmbedding U hU T := by
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCoreAction, OAI.KadisonKastler.regularCoreEmbedding