OAI/Combinatorics/SumProduct/Alignment/ProductExposure04.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ProductExposureLaw.outsideDomain line 17
2. def OAI.ProductExposureLaw.outsideLaw line 20
3. instance OAI.ProductExposureLaw.outsideLaw_probability line 23
4. def OAI.ProductExposureLaw.reassemble line 28
5. lemma OAI.ProductExposureLaw.outside_ae_domain line 31
6. lemma OAI.ProductExposureLaw.outside_weights_sum line 39
7. lemma OAI.ProductExposureLaw.joint_reassemble line 51
8. theorem OAI.ProductExposureLaw.joint_outside_disintegration line 106
9. theorem OAI.RoughArrayFace.source_full_earlier_face_decay line 149
10. theorem OAI.ConditionalDiagonal.select line 247