OAI/Analysis/IrrationalRotation/Product/IndependentKernelProduct.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Invariant233.KernelProduct.independent_isMarkov line 17
2. theorem OAI.Invariant233.KernelProduct.independent_apply line 21
3. theorem OAI.Invariant233.KernelProduct.compProd_map_pairCoordinates line 25
4. theorem OAI.Invariant233.KernelProduct.independent_coordinates line 54
5. theorem OAI.Invariant233.KernelProduct.coordinate_disintegration line 65
6. theorem OAI.Invariant233.KernelProduct.condDistrib_coordinates line 87
7. theorem OAI.Invariant233.KernelProduct.coordinate_pair_disintegration line 107
8. theorem OAI.Invariant233.KernelProduct.condDistrib_of_coordinate_disintegration line 131