OAI/Probability/StrongRayleigh/CharacteristicLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336AdditiveD139.CharacteristicLaw.map_restrict_eq_smul_of_characteristic line 20
2. theorem OAI.Problem336AdditiveD139.CharacteristicLaw.map_eq_of_event_characteristic line 32
3. theorem OAI.Problem336AdditiveD139.CharacteristicLaw.independent_of_restricted_law line 44
4. theorem OAI.Problem336AdditiveD139.CharacteristicLaw.law_and_independent_of_event_characteristic line 62
5. theorem OAI.Problem336AdditiveD139.CharacteristicLaw.indepFun_of_event_characteristic line 74