RegularCoreOperators.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Operators on the actual regular Hilbert space

The regular core acts on L²(ℝ,H), with a constant operator representation and multiplication by a measurable unitary field. The latter gives the gauge transformation used to write the core embedding as a faithful conjugate of the constant representation.

def OAI.KadisonKastler.regularConstantOperator line 30
Source documentation
Pointwise action of a constant bounded operator on a Hilbert-valued L² space.
```
def regularConstantOperator (μ : Measure D) (T : H →L[ℂ] H) :
    Lp H 2 μ →L[ℂ] Lp H 2 μ :=
…
```
theorem OAI.KadisonKastler.regularConstantOperator_apply_ae line 35
theorem OAI.KadisonKastler.regularConstantOperator_mul line 41
theorem OAI.KadisonKastler.regularConstantOperator_one line 55
theorem OAI.KadisonKastler.regularConstantOperator_star line 63
def OAI.KadisonKastler.regularConstantHom line 79
Source documentation
The constant copy of B(H) on a Hilbert-valued L² space.
```
def regularConstantHom (μ : Measure D) :
    (H →L[ℂ] H) →⋆ₐ[ℂ] (Lp H 2 μ →L[ℂ] Lp H 2 μ) where
…
```
theorem OAI.KadisonKastler.regularConstantHom_apply_ae line 102
theorem OAI.KadisonKastler.regularConstantHom_injective line 109
Source documentation
A finite positive-measure test set makes the constant representation faithful, without requiring a finite total measure.
```
theorem regularConstantHom_injective (μ : Measure D) (s : Set D)
    (hs : MeasurableSet s) (hfin : μ s ≠ ∞) (hpos : μ s ≠ 0) :
    Function.Injective (regularConstantHom (H := H) μ) := by
…
```
Mentions: OAI.KadisonKastler.regularConstantHom

def OAI.KadisonKastler.regularUnitaryFieldApply line 131

Source documentation

Multiplication of L² vectors by a measurable unitary field.

def regularUnitaryFieldApply (μ : Measure D) (U : D → unitary (H →L[ℂ] H))
    (hU : ∀ x, AEStronglyMeasurable (fun t => (U t : H →L[ℂ] H) x) μ)
    (f : Lp H 2 μ) : Lp H 2 μ :=
…

theorem OAI.KadisonKastler.regularUnitaryFieldApply_ae line 139
theorem OAI.KadisonKastler.norm_regularUnitaryFieldApply line 146

def OAI.KadisonKastler.regularUnitaryField line 157

Source documentation

The gauge operator as a genuine unitary on the regular Hilbert space.

def regularUnitaryField (μ : Measure D) (U : D → unitary (H →L[ℂ] H))
    (hU : ∀ x, AEStronglyMeasurable (fun t => (U t : H →L[ℂ] H) x) μ)
    (hUs : ∀ x, AEStronglyMeasurable (fun t => (star (U t) : H →L[ℂ] H) x) μ) :
    unitary (Lp H 2 μ →L[ℂ] Lp H 2 μ) :=
…

theorem OAI.KadisonKastler.regularUnitaryField_apply_ae line 203
abbrev OAI.KadisonKastler.RegularCoreHilbert line 213
Source documentation
The actual real-line regular Hilbert space.
```
abbrev RegularCoreHilbert (H : Type*) [NormedAddCommGroup H] :=
…
```
theorem OAI.KadisonKastler.real_regularConstantHom_injective line 216
theorem OAI.KadisonKastler.real_regularConstantHom_completelyIsometric line 224