RegularCoreFixed.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Fixed decomposable operators in the regular representation

The gauge transforms a decomposable operator fixed by U_s ⊗ ρ_s into a translation-fixed multiplier. The preceding scalar Fubini argument then makes it a constant operator, so the original operator belongs to the concrete regular image π(B(H)).

theorem OAI.KadisonKastler.RepresentsOperatorField.regular_gauge line 26

Source documentation

The gauge conjugation has the expected field formula.

theorem RepresentsOperatorField.regular_gauge
    {F : ℝ → H →L[ℂ] H} {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hF : RepresentsOperatorField volume F T) :
    RepresentsOperatorField volume
      (fun t => unitaryConj (U (Multiplicative.ofAdd t)) (F t))
      (unitaryConj (regularGauge U hU) T) := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.RepresentsOperatorField, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularGauge

theorem OAI.KadisonKastler.regularGauge_translation_fixed line 46
Source documentation
Fixedness passes through the exact gauge intertwining identity.
```
theorem regularGauge_translation_fixed
    {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hfixed : ∀ s, unitaryConj (regularCoreAction U s) T = T)
    (s : Multiplicative ℝ) :
    unitaryConj (regularRightTranslation (H := H) s)
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCoreAction, OAI.KadisonKastler.regularRightTranslation

theorem OAI.KadisonKastler.exists_regularCoreEmbedding_of_field_fixed line 59

Source documentation

A weakly measurable decomposable operator fixed by the common action belongs to the actual regular image.

theorem exists_regularCoreEmbedding_of_field_fixed [TopologicalSpace.SeparableSpace H]
    {F : ℝ → H →L[ℂ] H} {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hF : RepresentsOperatorField volume F T)
    (hmeas : ∀ ξ, AEStronglyMeasurable (fun t => F t ξ) volume)
    (hfixed : ∀ s, unitaryConj (regularCoreAction U s) T = T) :
    ∃ A : H →L[ℂ] H, T = regularCoreEmbedding U hU A := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.RepresentsOperatorField, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCoreAction, OAI.KadisonKastler.regularCoreEmbedding