OAI/Dynamics/EntropyCounterexample/SphereSquareFiber.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem340.SphereDoubling.sphereMap_eq_east_iff line 9
2. theorem OAI.Problem340.SphereDoubling.preimage_east line 43
3. theorem OAI.Problem340.SphereDoubling.ncard_preimage_east line 48
4. theorem OAI.Problem340.SphereDoubling.hasFDerivAt_complex_square_one line 52
5. theorem OAI.Problem340.SphereDoubling.hasFDerivAt_complex_square_neg_one line 60
6. theorem OAI.Problem340.SphereDoubling.det_fderiv_complex_square_one line 68
7. theorem OAI.Problem340.SphereDoubling.det_fderiv_complex_square_neg_one line 75
8. theorem OAI.Problem340.SphereDoubling.stereoCoordinate_east line 82
9. theorem OAI.Problem340.SphereDoubling.stereoCoordinate_west line 85
10. theorem OAI.Problem340.SphereDoubling.det_fderiv_complex_square_at_preimage_east line 88