OAI/Probability/Ballisticity/Estimates/CharacteristicProductLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.linearPhaseTest line 14
2. lemma OAI.DirectionalTransience.real_linear_apply line 24
3. lemma OAI.DirectionalTransience.charFunDual_gaussianReal line 28
4. lemma OAI.DirectionalTransience.product_linear_split line 40
5. lemma OAI.DirectionalTransience.product_normal_law_of_characteristics line 48
6. def OAI.DirectionalTransience.FullNormalJointPast line 97
7. lemma OAI.DirectionalTransience.fullNormalJointPast_of_cross line 105
8. lemma OAI.DirectionalTransience.measure_prod_shuffle line 133