OAI/Analysis/FiniteFactor/CrossedProduct/TorusCharacters.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceCharacter line 12
2. theorem OAI.FiniteFactor.sourceCharacter_zero line 18
3. theorem OAI.FiniteFactor.sourceCharacter_add line 22
4. theorem OAI.FiniteFactor.sourceCharacter_neg line 29
5. def OAI.FiniteFactor.sourceCharacterAlgebra line 44
6. theorem OAI.FiniteFactor.sourceCharacterAlgebra_span line 52
7. theorem OAI.FiniteFactor.sourceCharacter_single line 59
8. theorem OAI.FiniteFactor.sourceCharacterAlgebra_separates line 63
9. theorem OAI.FiniteFactor.sourceCharacter_span_dense line 73

   Source documentation

   Uniform density on the full countable product, with no finite-dimensional truncation assumption.

   theorem sourceCharacter_span_dense :
       (span ℂ (range sourceCharacter)).topologicalClosure = ⊤ := by
   …

   Mentions: OAI.FiniteFactor.sourceCharacter

10. abbrev OAI.FiniteFactor.sourceCharacterL2 line 80
11. theorem OAI.FiniteFactor.sourceCharacterL2_span_dense line 83