OperatorField.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.sourceMatrixGood line 12
def OAI.FiniteFactor.sourceFieldGoodSet line 19
Source documentation
A Borel good set, removing just one null set for algebra elements.
```
def sourceFieldGoodSet
    (H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate) :
    Set (SourceCoordinate → ℝ) :=
…
```
Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate
theorem OAI.FiniteFactor.sourceFieldGoodSet_measurable line 24
theorem OAI.FiniteFactor.sourceFieldGoodSet_good line 28
theorem OAI.FiniteFactor.sourceFieldGoodSet_ae line 34
def OAI.FiniteFactor.sourceOperatorField line 42
Source documentation
The actual bounded operator field, extended by zero on a Borel null set.
```
def sourceOperatorField
    (H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate)
    (x : SourceCoordinate → ℝ) : SourceFiberHilbert →L[ℂ] SourceFiberHilbert := by
…
```
Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceFiberHilbert
theorem OAI.FiniteFactor.sourceOperatorField_norm line 51
theorem OAI.FiniteFactor.sourceOperatorField_entry line 60
theorem OAI.FiniteFactor.sourceOperatorField_entry_measurable line 71
theorem OAI.FiniteFactor.sourceOperatorField_entries_ae line 78
Source documentation
Field entries recover the original coefficients on one conull set.
```
theorem sourceOperatorField_entries_ae (θ : SourceCoordinate → ℝ)
    {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hH : H ∈ sourceAlgebra θ) :
    ∀ᵐ x ∂sourceBaseMeasure, ∀ k n : ℤ,
      (sourceOperatorField H x (lp.single 2 n (1 : ℂ))) k = sourceMatrixEntry H k n x := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceOperatorField, OAI.FiniteFactor.sourceMatrixEntry