RegularCoreFields.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Bounded field multiplication and constant translation-fixed fields

Bounded measurable operator fields act on the actual vector-valued L² space. Finite-measure indicator tests recover their coefficients, so this action is faithful modulo almost-everywhere equality. A decomposable operator commuting with every real translation is a constant operator. No decomposability assertion for an arbitrary operator is assumed here.

theorem OAI.KadisonKastler.regularField_memLp line 27
def OAI.KadisonKastler.regularFieldApply line 36
theorem OAI.KadisonKastler.regularFieldApply_ae line 42
theorem OAI.KadisonKastler.norm_regularFieldApply_le line 49

def OAI.KadisonKastler.regularFieldOperator line 60

Source documentation

Multiplication by an essentially bounded, strongly measurable operator field, as a genuine bounded operator.

def regularFieldOperator (μ : Measure X) (F : X → H →L[ℂ] H)
    (hF : ∀ ξ, AEStronglyMeasurable (fun t => F t ξ) μ)
    (C : ℝ) (hC : ∀ᵐ t ∂μ, ‖F t‖ ≤ C) : Lp H 2 μ →L[ℂ] Lp H 2 μ :=
…

theorem OAI.KadisonKastler.regularFieldOperator_represents line 87
theorem OAI.KadisonKastler.norm_regularFieldOperator_le line 94

theorem OAI.KadisonKastler.RepresentsOperatorField.eval_eq_ae_on line 103

Source documentation

Indicator tests recover each vector coefficient of an operator field on a finite-measure set.

theorem RepresentsOperatorField.eval_eq_ae_on {μ : Measure X}
    {F G : X → H →L[ℂ] H} {T : Lp H 2 μ →L[ℂ] Lp H 2 μ}
    (hF : RepresentsOperatorField μ F T) (hG : RepresentsOperatorField μ G T)
    {s : Set X} (hs : MeasurableSet s) (hfinite : μ s ≠ ∞) (ξ : H) :
    ∀ᵐ t ∂μ, t ∈ s → F t ξ = G t ξ := by
…

Mentions: OAI.KadisonKastler.RepresentsOperatorField

theorem OAI.KadisonKastler.RepresentsOperatorField.eval_eq_ae_real line 119

Source documentation

Equality of actual real-line multiplication operators recovers each vector value almost everywhere.

theorem RepresentsOperatorField.eval_eq_ae_real
    {F G : ℝ → H →L[ℂ] H} {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hF : RepresentsOperatorField volume F T) (hG : RepresentsOperatorField volume G T)
    (ξ : H) : (fun t => F t ξ) =ᵐ[volume] fun t => G t ξ := by
…

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

theorem OAI.KadisonKastler.RepresentsOperatorField.field_eq_ae_real line 135

Source documentation

On a separable Hilbert space, equality of multiplication operators recovers the entire field almost everywhere.

theorem RepresentsOperatorField.field_eq_ae_real [TopologicalSpace.SeparableSpace H]
    {F G : ℝ → H →L[ℂ] H} {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hF : RepresentsOperatorField volume F T) (hG : RepresentsOperatorField volume G T) :
    F =ᵐ[volume] G := by
…

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

theorem OAI.KadisonKastler.RepresentsOperatorField.real_translate line 148

Source documentation

Translation conjugates an actual multiplication operator by shifting its field.

theorem RepresentsOperatorField.real_translate
    {F : ℝ → H →L[ℂ] H} {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hF : RepresentsOperatorField volume F T) (s : Multiplicative ℝ) :
    RepresentsOperatorField volume (fun t => F (t + s.toAdd))
      (unitaryConj (regularRightTranslation (H := H) s) T) := by
…

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

theorem OAI.KadisonKastler.constant_of_regularField_translation_fixed line 181
Source documentation
An actually decomposable operator fixed by every translation is a constant operator. Decomposability itself is not posited for arbitrary operators.
```
theorem constant_of_regularField_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)
    (hfixed : ∀ s, unitaryConj (regularRightTranslation (H := H) s) T = T) :
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.RepresentsOperatorField, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularRightTranslation