MeasurableHilbertCoordinates.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Measurability of countable Hilbert coordinates

Coordinatewise measurability implies norm-Borel measurability in a countable scalar Hilbert sum. Finite-coordinate sums give the required approximations.

theorem OAI.KadisonKastler.separable_scalarHilbertCoordinates line 23
Source documentation
The scalar Hilbert coordinate space for a countable index set is separable.
```
theorem separable_scalarHilbertCoordinates : SeparableSpace ℓ²(I, ℂ) := by
…
```
theorem OAI.KadisonKastler.measurable_hilbertCoordinates line 35
Source documentation
A field of Hilbert coordinate vectors is measurable if each scalar coordinate is.
```
theorem measurable_hilbertCoordinates (f : X → ℓ²(I, ℂ))
    (hf : ∀ i, Measurable fun x => f x i) : Measurable f := by
…
```

theorem OAI.KadisonKastler.measurable_rangeHilbertCoordinates line 53

Source documentation

Measurable columns make analysis in a variable range basis measurable.

theorem measurable_rangeHilbertCoordinates (P : X → H →L[ℂ] H)
    (B : ∀ x, HilbertBasis I ℂ (P x).range)
    (hB : ∀ i, Measurable fun x => (B x i : H))
    (v : ∀ x, (P x).range) (hv : Measurable fun x => (v x : H)) :
    Measurable fun x => (B x).repr (v x) := by
…

theorem OAI.KadisonKastler.measurable_rangeHilbertSynthesis line 65