OAI/Analysis/PeriodicLattice/Trajectories.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of trajectories and smooth flow estimates.

  1. theorem OAI.PeriodicLattice.Trajectories.unique line 22
  2. def OAI.PeriodicLattice.Profiles.accumulated line 74
  3. theorem OAI.PeriodicLattice.Profiles.accumulated_contDiff line 76
  4. theorem OAI.PeriodicLattice.Profiles.accumulated_in_collar line 85
  5. theorem OAI.PeriodicLattice.Profiles.accumulated_eventually line 103
  6. theorem OAI.PeriodicLattice.Profiles.accumulated_on_slot line 111
  7. theorem OAI.PeriodicLattice.Profiles.accumulated_at_integer line 116
  8. theorem OAI.PeriodicLattice.Profiles.accumulated_hasDerivAt line 122