Entries.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.FiniteFactor.sourceBaseMeasure line 11
theorem OAI.FiniteFactor.source_ae_all_fibers line 15
Source documentation
A product almost-everywhere identity holds on every integer fiber.
```
theorem source_ae_all_fibers {p : (SourceCoordinate → ℝ) × ℤ → Prop}
    (hp : ∀ᵐ z ∂sourceMeasure SourceCoordinate, p z) :
    ∀ᵐ x ∂sourceBaseMeasure, ∀ n : ℤ, p (x,n) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceMeasure, OAI.FiniteFactor.sourceBaseMeasure
def OAI.FiniteFactor.sourceBasis line 21
Source documentation
Constant coordinate vector, realized in the original source L2 space.
```
def sourceBasis (n : ℤ) : SourceHilbert SourceCoordinate :=
…
```
Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate
theorem OAI.FiniteFactor.sourceBasis_coe line 24
theorem OAI.FiniteFactor.sourceBasis_zero line 30
def OAI.FiniteFactor.sourceMatrixEntry line 33
Source documentation
Actual matrix coefficients obtained by applying H to constant e_n.
```
def sourceMatrixEntry (H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate)
    (k n : ℤ) (x : SourceCoordinate → ℝ) : ℂ := (H (sourceBasis n)) (x,k)
```
Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceBasis
theorem OAI.FiniteFactor.sourceScalar_apply_ae line 36
theorem OAI.FiniteFactor.sourceScalar_indicator_basis line 46
theorem OAI.FiniteFactor.sourceMatrixEntry_localize line 57
Source documentation
Localizing an input coordinate localizes every output coordinate by the same base indicator. This uses the proved commutant of the actual algebra.
```
theorem sourceMatrixEntry_localize (θ : SourceCoordinate → ℝ)
    {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hH : H ∈ sourceAlgebra θ) (A : Set (SourceCoordinate → ℝ)) (hA : MeasurableSet A)
    (n : ℤ) : ∀ᵐ x ∂sourceBaseMeasure, ∀ k : ℤ,
      (H (sourceFiberIndicator A hA n)) (x,k) =
        A.indicator (sourceMatrixEntry H k n) x := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceFiberIndicator, OAI.FiniteFactor.sourceMatrixEntry