OAI/Analysis/FiniteFactor/CrossedProduct/FiniteVectors.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceFiniteVector line 12

   Source documentation

   Finite coordinate vectors as actual constant-base L2 vectors.

   def sourceFiniteVector (s : Finset ℤ) (a : ℤ → ℂ) : SourceHilbert SourceCoordinate :=
   …

   Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate

2. theorem OAI.FiniteFactor.sourceHilbert_sum_coe line 15
3. theorem OAI.FiniteFactor.sourceFiniteVector_coe line 29
4. theorem OAI.FiniteFactor.sourceFiniteVector_image_coe line 44
5. theorem OAI.FiniteFactor.sourceFiniteVector_energy line 62