OAI/Geometry/NearbyLagrangian/TimeMesh.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite time meshes and prepared mixed steps.

  1. theorem OAI.NearbyLagrangian.Transport.compact_flow_step_small line 21
  2. theorem OAI.NearbyLagrangian.Transport.compact_flow_step_displacement line 62
  3. theorem OAI.NearbyLagrangian.Transport.exists_uniform_time_subdivision line 85
  4. lemma OAI.NearbyLagrangian.Transport.exists_equal_time_mesh line 123
  5. theorem OAI.NearbyLagrangian.Transport.exists_uniform_time_subdivision_both line 142
  6. structure OAI.NearbyLagrangian.Transport.PreparedMixedStep line 168
  7. theorem OAI.NearbyLagrangian.Transport.exists_finite_prepared_steps line 186
  8. theorem OAI.NearbyLagrangian.Transport.PreparedMixedStep.exists_stepData line 255