OAI/Dynamics/EntropyCounterexample/NormalizedPrediction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem340.NormalizedPrediction.contDiffOn_iterate line 17
2. theorem OAI.Problem340.NormalizedPrediction.norm_fderiv_iterate_le line 27
3. theorem OAI.Problem340.NormalizedPrediction.norm_fderiv_iterate_le_scaled line 41
4. def OAI.Problem340.NormalizedPrediction.clock line 81
5. theorem OAI.Problem340.NormalizedPrediction.contDiffOn_clock line 84
6. theorem OAI.Problem340.NormalizedPrediction.norm_fderiv_clock_le line 89
7. theorem OAI.Problem340.NormalizedPrediction.norm_fderiv_clock_le_scaled line 103
8. theorem OAI.Problem340.NormalizedPrediction.clock_eq_original_on_sphere line 123