FieldRepresentation.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.fiberCoordinates_stronglyMeasurable line 12
Source documentation
Coordinate measurability suffices for strong measurability in l2(Z).
```
theorem fiberCoordinates_stronglyMeasurable {X : Type*} [MeasurableSpace X]
    (f : X → SourceFiberHilbert) (hf : ∀ n : ℤ, Measurable (fun x => f x n)) :
    StronglyMeasurable f := by
…
```
Mentions: OAI.FiniteFactor.SourceFiberHilbert
theorem OAI.FiniteFactor.sourceOperatorField_basis_stronglyMeasurable line 29
Source documentation
Every basis column of the actual field is a strongly measurable l2 vector.
```
theorem sourceOperatorField_basis_stronglyMeasurable
    (H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate) (n : ℤ) :
    StronglyMeasurable (fun x => sourceOperatorField H x (lp.single 2 n (1 : ℂ))) :=
…
```
Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceOperatorField
theorem OAI.FiniteFactor.sourceOperatorField_stronglyMeasurable line 34
theorem OAI.FiniteFactor.source_fiber_memℓp line 50
Source documentation
Fubini puts almost every actual L2 section in l2(Z).
```
theorem source_fiber_memℓp (f : SourceHilbert SourceCoordinate) :
    ∀ᵐ x ∂sourceBaseMeasure, Memℓp (fun n : ℤ => f (x,n)) 2 := by
…
```
Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceBaseMeasure
def OAI.FiniteFactor.sourceFiberVector line 58
Source documentation
A fiber vector with an irrelevant zero value on the exceptional null set.
```
def sourceFiberVector (f : SourceHilbert SourceCoordinate) (x : SourceCoordinate → ℝ) :
    SourceFiberHilbert := by
…
```
Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceFiberHilbert
theorem OAI.FiniteFactor.sourceFiberVector_coe line 63
theorem OAI.FiniteFactor.sourceOperatorField_represents line 70
Source documentation
The constructed field acts as the original operator on every source L2 vector. Neither decomposability nor a replacement representation is assumed.
```
theorem sourceOperatorField_represents (θ : SourceCoordinate → ℝ)
    {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hH : H ∈ sourceAlgebra θ) (f : SourceHilbert SourceCoordinate) :
    ∀ᵐ x ∂sourceBaseMeasure,
      sourceFiberVector (H f) x = sourceOperatorField H x (sourceFiberVector f x) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceFiberVector, OAI.FiniteFactor.sourceOperatorField