RegularCoreDensePeriods.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Dense periods of bounded regular coefficient fields

Strong continuity of translations on the actual L² space extends commutation from any dense family of translations to all translations. Consequently a bounded measurable field with dense periods is constant almost everywhere. In particular, two incommensurable scalar periods suffice, as required by the two-frequency modular-core argument.

theorem OAI.KadisonKastler.continuous_regularTranslateApply line 28
Source documentation
Real translations are strongly continuous on the actual regular Hilbert space.
```
theorem continuous_regularTranslateApply (f : RegularCoreHilbert H) :
    Continuous (fun s : ℝ => regularTranslateApply s f) := by
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularTranslateApply
theorem OAI.KadisonKastler.regularTranslation_commute_of_dense line 39
Source documentation
A bounded operator commuting with a dense set of translations commutes with every translation.
```
theorem regularTranslation_commute_of_dense
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    {S : Set ℝ} (hS : Dense S)
    (hcomm : ∀ s ∈ S, Commute T
      (regularRightTranslation (H := H) (Multiplicative.ofAdd s) :
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularRightTranslation

theorem OAI.KadisonKastler.constant_of_regularField_dense_translation_fixed line 60

Source documentation

A decomposable operator fixed by a dense set of translations has an almost-everywhere constant field.

theorem constant_of_regularField_dense_translation_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)
    {S : Set ℝ} (hS : Dense S)
    (hfixed : ∀ s ∈ S, unitaryConj
      (regularRightTranslation (H := H) (Multiplicative.ofAdd s)) T = T) :
…

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

theorem OAI.KadisonKastler.bounded_operatorField_dense_periods_const line 85

Source documentation

Bounded measurable operator fields with a dense set of periods are constant almost everywhere.

theorem bounded_operatorField_dense_periods_const
    [TopologicalSpace.SeparableSpace H]
    (F : ℝ → H →L[ℂ] H)
    (hmeas : ∀ ξ, AEStronglyMeasurable (fun t => F t ξ) volume)
    (C : ℝ) (hbound : ∀ᵐ t ∂volume, ‖F t‖ ≤ C)
    {S : Set ℝ} (hS : Dense S)
    (hperiod : ∀ s ∈ S, (fun t => F (t + s)) =ᵐ[volume] F) :
    ∃ A : H →L[ℂ] H, F =ᵐ[volume] fun _ => A := by
…

theorem OAI.KadisonKastler.bounded_scalar_dense_periods_const line 108

Source documentation

Scalar bounded coefficient fields are a special case of the actual operator-field construction.

theorem bounded_scalar_dense_periods_const
    (f : ℝ → ℂ) (hmeas : AEStronglyMeasurable f volume)
    (C : ℝ) (hbound : ∀ᵐ t ∂volume, ‖f t‖ ≤ C)
    {S : Set ℝ} (hS : Dense S)
    (hperiod : ∀ s ∈ S, (fun t => f (t + s)) =ᵐ[volume] f) :
    ∃ c : ℂ, f =ᵐ[volume] fun _ => c := by
…

def OAI.KadisonKastler.scalarAEPeriods line 129
Source documentation
Almost-everywhere periods form an actual additive subgroup.
```
def scalarAEPeriods (f : ℝ → ℂ) : AddSubgroup ℝ where
…
```

theorem OAI.KadisonKastler.bounded_scalar_two_periods_const line 146

Source documentation

Two periods with irrational ratio force any essentially bounded measurable scalar field to be constant almost everywhere.

theorem bounded_scalar_two_periods_const
    (f : ℝ → ℂ) (hmeas : AEStronglyMeasurable f volume)
    (C : ℝ) (hbound : ∀ᵐ t ∂volume, ‖f t‖ ≤ C)
    {a b : ℝ} (hirr : Irrational (a / b))
    (ha : (fun t => f (t + a)) =ᵐ[volume] f)
    (hb : (fun t => f (t + b)) =ᵐ[volume] f) :
    ∃ c : ℂ, f =ᵐ[volume] fun _ => c := by
…

theorem OAI.KadisonKastler.bounded_operatorField_two_periods_const line 169

Source documentation

Two incommensurable periods scalarize an entire bounded measurable operator field, with one common exceptional null set.

theorem bounded_operatorField_two_periods_const
    [TopologicalSpace.SeparableSpace H]
    (F : ℝ → H →L[ℂ] H)
    (hmeas : ∀ ξ, AEStronglyMeasurable (fun t => F t ξ) volume)
    (C : ℝ) (hbound : ∀ᵐ t ∂volume, ‖F t‖ ≤ C)
    {a b : ℝ} (hirr : Irrational (a / b))
    (ha : (fun t => F (t + a)) =ᵐ[volume] F)
    (hb : (fun t => F (t + b)) =ᵐ[volume] F) :
    ∃ A : H →L[ℂ] H, F =ᵐ[volume] fun _ => A := by
…