OAI/Analysis/BrownMeasure/ConcreteTrace.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteFactor.SourceCStar line 13
2. instance OAI.FiniteFactor.sourceCStar_closed line 14
3. instance OAI.FiniteFactor.sourceCStar_nontrivial line 18
4. def OAI.FiniteFactor.sourceRealTrace line 26
5. lemma OAI.FiniteFactor.sourceRealTrace_apply line 37
6. lemma OAI.FiniteFactor.sourceRealTrace_cyclic line 39
7. lemma OAI.FiniteFactor.sourceRealTrace_star line 42
8. lemma OAI.FiniteFactor.sourceOperator_trace_pow_zero line 48
9. def OAI.FiniteFactor.sourceCStarOperator line 56
10. lemma OAI.FiniteFactor.sourceCStarOperator_root line 59
11. lemma OAI.FiniteFactor.sourceOperator_one_sub_isUnit line 63
12. lemma OAI.FiniteFactor.sourceOperator_trace_log_square_one_sub line 68