OAI/Analysis/FiniteFactor/Matrix/Action.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceFiberInner line 11
2. theorem OAI.FiniteFactor.sourceFiberInner_integrable line 14
3. theorem OAI.FiniteFactor.source_inner_fiber line 18
4. theorem OAI.FiniteFactor.sourceScalar_indicator_inner line 22
5. theorem OAI.FiniteFactor.source_coordinate_action_inner line 43

   Source documentation

   The scalar distribution identity determining every output coordinate of H.

   theorem source_coordinate_action_inner (θ : SourceCoordinate → ℝ)
       {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hH : H ∈ sourceAlgebra θ) (f : SourceHilbert SourceCoordinate) (k : ℤ) :
       (fun x => (H f) (x,k)) =ᵐ[sourceBaseMeasure]
         sourceFiberInner ((star H) (sourceBasis k)) f := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceFiberInner, OAI.FiniteFactor.sourceBasis

6. theorem OAI.FiniteFactor.sourceMatrix_action line 64

   Source documentation

   Actual action on arbitrary L2 input, expressed through the constructed matrix entries. The counting integral is an absolutely convergent series a.e.

   theorem sourceMatrix_action (θ : SourceCoordinate → ℝ)
       {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hH : H ∈ sourceAlgebra θ) (f : SourceHilbert SourceCoordinate) (k : ℤ) :
       (fun x => (H f) (x,k)) =ᵐ[sourceBaseMeasure]
         fun x => ∫ n : ℤ, sourceMatrixEntry H k n x * f (x,n) ∂Measure.count := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceMatrixEntry

7. theorem OAI.FiniteFactor.sourceMatrix_action_integrable line 84

   Source documentation

   The matrix action is absolutely integrable over the counting measure.

   theorem sourceMatrix_action_integrable (θ : SourceCoordinate → ℝ)
       {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hH : H ∈ sourceAlgebra θ) (f : SourceHilbert SourceCoordinate) (k : ℤ) :
       ∀ᵐ x ∂sourceBaseMeasure,
         Integrable (fun n : ℤ => sourceMatrixEntry H k n x * f (x,n)) Measure.count := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceMatrixEntry

8. theorem OAI.FiniteFactor.sourceMatrix_action_tsum line 102
9. theorem OAI.FiniteFactor.sourceMatrix_mul line 113

   Source documentation

   Products are given by the matrix product on a single conull base set.

   theorem sourceMatrix_mul (θ : SourceCoordinate → ℝ)
       {H B : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hH : H ∈ sourceAlgebra θ) :
       ∀ᵐ x ∂sourceBaseMeasure, ∀ k n : ℤ,
         sourceMatrixEntry (H * B) k n x =
           ∫ r : ℤ, sourceMatrixEntry H k r x * sourceMatrixEntry B r n x ∂Measure.count := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceMatrixEntry