OAI/Analysis/BrownMeasure/UnitDeterminant.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FiniteFactor.sourceVacuumFunctional_mono line 15
2. lemma OAI.FiniteFactor.product_abs_isUnit line 24
3. lemma OAI.FiniteFactor.product_abs_spectrum_pos line 29
4. lemma OAI.FiniteFactor.logarithmCutoff_cfc_eq_log line 35
5. lemma OAI.FiniteFactor.FugledeKadisonDeterminant_of_isUnit line 53