OAI/Analysis/BrownMeasure/Modulus.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FiniteFactor.sourceShift_eq_transport line 14
2. lemma OAI.FiniteFactor.sourceShift_unitary line 28
3. def OAI.FiniteFactor.sourceWeightSqrtBase line 33
4. lemma OAI.FiniteFactor.sourceWeight_positive line 44
5. lemma OAI.FiniteFactor.sourceOperator_abs line 65
6. lemma OAI.FiniteFactor.sourcePolarFamily_zero line 80
7. lemma OAI.FiniteFactor.sourceTransport_conjugate_pi line 93