RegularCoreHilbertSum.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Scalar Hilbert coordinates on the regular representation

A scalar Hilbert basis of L²(ℝ) gives an actual Hilbert direct-sum decomposition of L²(ℝ,H). Constant operators act on each summand by their original action on H.

def OAI.KadisonKastler.regularTensorVector line 25
Source documentation
An elementary scalar-vector tensor, as a continuous bilinear map.
```
def regularTensorVector :
    Lp ℂ 2 (volume : Measure ℝ) →L[ℂ] H →L[ℂ] RegularCoreHilbert H :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularTensorVector_apply_ae line 31
theorem OAI.KadisonKastler.inner_regularTensorVector line 36
theorem OAI.KadisonKastler.norm_regularTensorVector line 52
def OAI.KadisonKastler.regularBasisSummand line 65
Source documentation
The copy of H belonging to one scalar basis vector.
```
def regularBasisSummand (b : HilbertBasis ι ℂ (Lp ℂ 2 (volume : Measure ℝ)))
    (i : ι) : H →ₗᵢ[ℂ] RegularCoreHilbert H where
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularBasisSummand_orthogonal line 73
theorem OAI.KadisonKastler.regularBasisSummand_total line 81
theorem OAI.KadisonKastler.regularHilbertSum line 123
Source documentation
The regular space is the Hilbert sum of the scalar-basis copies of H.
```
theorem regularHilbertSum (b : HilbertBasis ι ℂ (Lp ℂ 2 (volume : Measure ℝ))) :
    IsHilbertSum ℂ (fun _ : ι => H) (regularBasisSummand b) :=
…
```
Mentions: OAI.KadisonKastler.regularBasisSummand
def OAI.KadisonKastler.regularHilbertCoordinates line 128
Source documentation
Actual Hilbert coordinates on the regular representation.
```
def regularHilbertCoordinates (b : HilbertBasis ι ℂ (Lp ℂ 2 (volume : Measure ℝ))) :
    RegularCoreHilbert H ≃ₗᵢ[ℂ] lp (fun _ : ι => H) 2 :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularConstantHom_tensorVector line 132
theorem OAI.KadisonKastler.regularHilbertCoordinates_constant line 144
Source documentation
In scalar Hilbert coordinates, the constant operator is exactly the coordinatewise operator.
```
theorem regularHilbertCoordinates_constant
    (b : HilbertBasis ℕ ℂ (Lp ℂ 2 (volume : Measure ℝ))) (T : H →L[ℂ] H) :
    (regularHilbertCoordinates b).conjStarAlgEquiv
      (regularConstantHom (volume : Measure ℝ) T) = l2Diagonal T := by
…
```
Mentions: OAI.KadisonKastler.regularHilbertCoordinates, OAI.KadisonKastler.regularConstantHom, OAI.KadisonKastler.l2Diagonal