OAI/Analysis/LienardCycles/GlobalODE.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuinticLienard.GlobalODE.bounded_lipschitz_global_solution line 17
2. def OAI.QuinticLienard.GlobalODE.flow line 68
3. theorem OAI.QuinticLienard.GlobalODE.flow_zero line 71
4. theorem OAI.QuinticLienard.GlobalODE.flow_deriv line 74
5. theorem OAI.QuinticLienard.GlobalODE.flow_unique line 78
6. theorem OAI.QuinticLienard.GlobalODE.flow_add line 86
7. theorem OAI.QuinticLienard.GlobalODE.flow_lipschitz_time line 94
8. theorem OAI.QuinticLienard.GlobalODE.flow_dist_initial line 101
9. theorem OAI.QuinticLienard.GlobalODE.continuous_flow line 120
10. theorem OAI.QuinticLienard.GlobalODE.local_family_eq line 136
11. theorem OAI.QuinticLienard.GlobalODE.analytic_flow_on_trajectory line 160
12. theorem OAI.QuinticLienard.GlobalODE.exists_bounded_lipschitz_cutoff line 203
13. theorem OAI.QuinticLienard.GlobalODE.exists_bounded_lipschitz_cutoff_on line 222
14. theorem OAI.QuinticLienard.GlobalODE.analytic_family_along_compact_solution line 257