OAI/Analysis/PeriodicLattice/FluidLift.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Periodic fluid lift of the planar dynamics.

  1. theorem OAI.PeriodicLattice.TorusCalculus.mk_surjective line 18
  2. theorem OAI.PeriodicLattice.TorusCalculus.mk_add line 24
  3. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_cover line 28
  4. theorem OAI.PeriodicLattice.TorusCalculus.periodic_deriv line 34
  5. theorem OAI.PeriodicLattice.TorusCalculus.contDiff_partial line 42
  6. def OAI.PeriodicLattice.FluidLift.eta line 57
  7. def OAI.PeriodicLattice.FluidLift.slope line 60
  8. theorem OAI.PeriodicLattice.FluidLift.eta_contDiff line 64
  9. theorem OAI.PeriodicLattice.FluidLift.slope_contDiff line 67
  10. theorem OAI.PeriodicLattice.FluidLift.eta_periodic line 70
  11. theorem OAI.PeriodicLattice.FluidLift.slope_periodic line 76
  12. theorem OAI.PeriodicLattice.FluidLift.eta_hasDerivAt line 82
  13. theorem OAI.PeriodicLattice.FluidLift.eta_center line 88
  14. theorem OAI.PeriodicLattice.FluidLift.slope_center line 89
  15. def OAI.PeriodicLattice.FluidLift.v line 91
  16. def OAI.PeriodicLattice.FluidLift.a line 92
  17. def OAI.PeriodicLattice.FluidLift.b line 93
  18. def OAI.PeriodicLattice.FluidLift.bdy line 94
  19. theorem OAI.PeriodicLattice.FluidLift.velocity_eq line 96
  20. theorem OAI.PeriodicLattice.FluidLift.v_contDiff line 99
  21. theorem OAI.PeriodicLattice.FluidLift.a_contDiff line 103
  22. theorem OAI.PeriodicLattice.FluidLift.b_contDiff line 105
  23. theorem OAI.PeriodicLattice.FluidLift.bdy_contDiff line 107
  24. theorem OAI.PeriodicLattice.FluidLift.a_periodic line 110
  25. theorem OAI.PeriodicLattice.FluidLift.b_periodic line 113
  26. theorem OAI.PeriodicLattice.FluidLift.bdy_periodic line 116
  27. def OAI.PeriodicLattice.FluidLift.velocity line 119
  28. theorem OAI.PeriodicLattice.FluidLift.velocity_cover line 127
  29. theorem OAI.PeriodicLattice.FluidLift.velocity_contDiff line 133
  30. theorem OAI.PeriodicLattice.FluidLift.velocity_smooth line 147
  31. theorem OAI.PeriodicLattice.FluidLift.velocity_on_plane line 149
  32. theorem OAI.PeriodicLattice.FluidLift.b_hasDerivAt line 155
  33. theorem OAI.PeriodicLattice.FluidLift.divergence_zero line 158
  34. theorem OAI.PeriodicLattice.FluidLift.velocity_solenoidal line 181
  35. theorem OAI.PeriodicLattice.FluidLift.velocity_start line 184
  36. def OAI.PeriodicLattice.FluidLift.path line 194
  37. theorem OAI.PeriodicLattice.FluidLift.path_contDiff line 196
  38. theorem OAI.PeriodicLattice.FluidLift.path_start line 204
  39. theorem OAI.PeriodicLattice.FluidLift.path_hasDerivAt line 208
  40. theorem OAI.PeriodicLattice.FluidLift.path_isParticle line 230
  41. theorem OAI.PeriodicLattice.FluidLift.path_unique line 233
  42. theorem OAI.PeriodicLattice.FluidLift.path_event_iff line 240
  43. theorem OAI.PeriodicLattice.FluidLift.eta_half_shift line 243
  44. theorem OAI.PeriodicLattice.FluidLift.slope_half_shift line 248
  45. theorem OAI.PeriodicLattice.FluidLift.velocity_half_shift line 253
  46. theorem OAI.PeriodicLattice.FluidLift.velocity_meanZero line 263