OAI/Dynamics/EntropyCounterexample/SpherePerturbation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem340.perturbedSquare line 12
2. theorem OAI.Problem340.perturbedSquare_infty line 15
3. theorem OAI.Problem340.perturbedSquare_coe line 18
4. theorem OAI.Problem340.tendsto_norm_perturbedSquare line 21
5. theorem OAI.Problem340.continuous_perturbedSquare line 37
6. def OAI.Problem340.perturbedSquareMap line 69
7. def OAI.Problem340.perturbedSquareHomotopy line 74
8. theorem OAI.Problem340.perturbedSquareMap_homotopic line 86