OAI/Analysis/PeriodicLattice/Planar.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Planar velocity fields implementing the encoded dynamics.

  1. abbrev OAI.PeriodicLattice.Planar.Point line 19
  2. def OAI.PeriodicLattice.Planar.slot line 21
  3. def OAI.PeriodicLattice.Planar.coefficients line 27
  4. def OAI.PeriodicLattice.Planar.field line 31
  5. theorem OAI.PeriodicLattice.Planar.slot_contDiff line 34
  6. theorem OAI.PeriodicLattice.Planar.field_contDiff line 39
  7. theorem OAI.PeriodicLattice.Planar.field_at_start line 48
  8. theorem OAI.PeriodicLattice.Planar.field_on_loader line 51
  9. theorem OAI.PeriodicLattice.Planar.field_on_slot line 57
  10. theorem OAI.PeriodicLattice.Planar.field_periodic_y line 66
  11. def OAI.PeriodicLattice.Planar.slotCurve line 81
  12. theorem OAI.PeriodicLattice.Planar.slotCurve_hasDerivAt line 85