OAI/Analysis/BrownMeasure/Polar.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourcePolarBase line 12
2. def OAI.FiniteFactor.sourcePolarFamily line 21
3. lemma OAI.FiniteFactor.sourcePolarFamily_selfAdjoint line 24
4. lemma OAI.FiniteFactor.sourcePolarFamily_jointPurePoint line 30
5. lemma OAI.FiniteFactor.sourcePolarFamily_finite_atomic line 51