OAI/Probability/StrongRayleigh/FiniteGaussianCharacteristic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336AdditiveD139.CharacteristicLaw.charFun_pi_centered_gaussian line 16
2. theorem OAI.Problem336AdditiveD139.CharacteristicLaw.map_restrict_eq_gaussian_pi_of_characteristic line 34
3. theorem OAI.Problem336AdditiveD139.CharacteristicLaw.gaussian_pi_law_and_independent_of_event_characteristic line 52