OAI/Analysis/PeriodicLattice/PlanarFlow.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Planar trajectories, support control and dynamical identities.

  1. def OAI.PeriodicLattice.Planar.codes line 20
  2. theorem OAI.PeriodicLattice.Planar.codes_bound line 24
  3. theorem OAI.PeriodicLattice.Planar.table_residue line 33
  4. theorem OAI.PeriodicLattice.Planar.table_history line 39
  5. def OAI.PeriodicLattice.Planar.increments line 46
  6. def OAI.PeriodicLattice.Planar.curve line 53
  7. theorem OAI.PeriodicLattice.Planar.curve_contDiff line 56
  8. theorem OAI.PeriodicLattice.Planar.curve_start line 59
  9. theorem OAI.PeriodicLattice.Planar.curve_succ line 64
  10. theorem OAI.PeriodicLattice.Planar.curve_on_slot line 70
  11. theorem OAI.PeriodicLattice.Planar.curve_y_integer line 75
  12. theorem OAI.PeriodicLattice.Planar.curve_y_slot line 90
  13. theorem OAI.PeriodicLattice.Planar.curve_plateau line 98
  14. def OAI.PeriodicLattice.Planar.ruleField line 114
  15. theorem OAI.PeriodicLattice.Planar.coefficients_on_curve line 117
  16. theorem OAI.PeriodicLattice.Planar.curve_solves line 139
  17. theorem OAI.PeriodicLattice.Planar.curve_unique line 159
  18. theorem OAI.PeriodicLattice.Planar.curve_x_before line 180
  19. theorem OAI.PeriodicLattice.Planar.curve_x_loader line 197
  20. theorem OAI.PeriodicLattice.Planar.curve_x_slot line 202
  21. theorem OAI.PeriodicLattice.Planar.curve_no_signal line 212
  22. theorem OAI.PeriodicLattice.Planar.curve_first_signal line 228
  23. def OAI.PeriodicLattice.Planar.embed line 236
  24. theorem OAI.PeriodicLattice.Planar.embed_first line 238
  25. theorem OAI.PeriodicLattice.Planar.curve_event_iff line 240
  26. theorem OAI.PeriodicLattice.Profiles.iteratedDeriv_pair line 273
  27. theorem OAI.PeriodicLattice.Planar.slot_iteratedDeriv line 296
  28. theorem OAI.PeriodicLattice.Planar.slot_derivative_bound line 316
  29. theorem OAI.PeriodicLattice.Planar.field_slot_derivative_bound line 378
  30. def OAI.PeriodicLattice.Planar.planarBound line 394
  31. theorem OAI.PeriodicLattice.Planar.field_weighted_derivative_bound line 397
  32. theorem OAI.PeriodicLattice.Planar.field_rapid line 449