SpatialFieldPeriods.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Tensor coefficients turn central commutation into frequency periods

In Fourier coordinates a site eigenoperator is a constant second-leg operator followed by a frequency translation. Commuting with it forces an actual first-leg coefficient field to have that period. Two incommensurable site frequencies therefore make the field constant.

theorem OAI.KadisonKastler.spatialTensorOp_left_injective line 26

Source documentation

A nonzero site operator detects its first tensor coefficient.

theorem spatialTensorOp_left_injective (b : K →L[ℂ] K) (hb : b ≠ 0) :
    Function.Injective (fun a : H →L[ℂ] H => spatialTensorOp a b) := by
…

theorem OAI.KadisonKastler.RepresentsOperatorField.intertwine_translation line 51

Source documentation

Commutation with a constant coefficient followed by translation gives an almost-everywhere field intertwining identity.

theorem RepresentsOperatorField.intertwine_translation
    [TopologicalSpace.SeparableSpace E]
    {F : ℝ → E →L[ℂ] E}
    {T : RegularCoreHilbert E →L[ℂ] RegularCoreHilbert E}
    (hF : RepresentsOperatorField volume F T) (b : E →L[ℂ] E) (s : ℝ)
    (hcomm : Commute T (regularConstantHom volume b *
      (regularRightTranslation (H := E) (Multiplicative.ofAdd s) :
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.RepresentsOperatorField, OAI.KadisonKastler.regularConstantHom, OAI.KadisonKastler.regularRightTranslation

theorem OAI.KadisonKastler.spatialField_period_of_commute line 90

Source documentation

A nonzero site eigenoperator forces its frequency to be a period of the first-leg coefficient field.

theorem spatialField_period_of_commute
    [TopologicalSpace.SeparableSpace (SpatialHilbert H K)]
    {F : ℝ → H →L[ℂ] H}
    {T : RegularCoreHilbert (SpatialHilbert H K) →L[ℂ]
      RegularCoreHilbert (SpatialHilbert H K)}
    (hF : RepresentsOperatorField volume (fun t => spatialLeft (K := K) (F t)) T)
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.RepresentsOperatorField, OAI.KadisonKastler.spatialLeft

theorem OAI.KadisonKastler.spatialField_constant_of_two_shifts line 112

Source documentation

The two site frequencies make a represented spatial coefficient field constant. No factoriality or core classification is assumed.

theorem spatialField_constant_of_two_shifts
    [TopologicalSpace.SeparableSpace H]
    [TopologicalSpace.SeparableSpace (SpatialHilbert H K)]
    {F : ℝ → H →L[ℂ] H}
    {T : RegularCoreHilbert (SpatialHilbert H K) →L[ℂ]
      RegularCoreHilbert (SpatialHilbert H K)}
    (hF : RepresentsOperatorField volume (fun t => spatialLeft (K := K) (F t)) T)
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.RepresentsOperatorField, OAI.KadisonKastler.spatialLeft