OAI/Analysis/BrownMeasure/Determinant.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FiniteFactor.sourceLog_measurable line 14
2. lemma OAI.FiniteFactor.sourceWeight_cfc line 22
3. lemma OAI.FiniteFactor.logarithmCutoff_exp_neg line 31
4. lemma OAI.FiniteFactor.sourceLog_trunc_integrable line 38
5. lemma OAI.FiniteFactor.sourceDeterminant_trace_logCutoff line 45
6. lemma OAI.FiniteFactor.sourceLog_trunc_antibounded line 60
7. theorem OAI.FiniteFactor.sourceOperator_determinant_zero line 89