OAI/Analysis/IrrationalRotation/Product/IndependentCoordinateConditioning.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.CoordinateConditioning.integral_finset_prod line 19
2. theorem OAI.Invariant233.CoordinateConditioning.integrable_finset_prod line 38
3. theorem OAI.Invariant233.CoordinateConditioning.prod_extend line 48
4. theorem OAI.Invariant233.CoordinateConditioning.cylinder_indicator_prod line 56
5. theorem OAI.Invariant233.CoordinateConditioning.setIntegral_cylinder_prod_eq line 82
6. theorem OAI.Invariant233.CoordinateConditioning.setIntegral_observed_prod_eq line 126
7. theorem OAI.Invariant233.CoordinateConditioning.condExp_finset_prod line 177
8. theorem OAI.Invariant233.CoordinateConditioning.condExp_label_product line 212
9. theorem OAI.Invariant233.CoordinateConditioning.condExp_label_inter line 243
10. theorem OAI.Invariant233.CoordinateConditioning.iCondIndepFun_labels line 263
11. theorem OAI.Invariant233.CoordinateConditioning.condExp_label_inter_of_disintegration line 302