OAI/Geometry/NearbyLagrangian/HomogeneousTails.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform tame bounds for homogeneous tails and flat evolutions.

  1. lemma OAI.NearbyLagrangian.Transport.baseDifferential_homogeneous_scale line 19
  2. lemma OAI.NearbyLagrangian.Transport.verticalDifferential_homogeneous_scale line 33
  3. lemma OAI.NearbyLagrangian.Transport.compact_positive_lower line 55
  4. theorem OAI.NearbyLagrangian.Transport.tameOn_of_compact_homogeneous_tail line 70
  5. lemma OAI.NearbyLagrangian.Transport.flatTimeField_spatial_support line 181
  6. theorem OAI.NearbyLagrangian.Transport.exists_flat_smooth_evolution line 190
  7. lemma OAI.NearbyLagrangian.Transport.flat_evolution_agrees line 205
  8. lemma OAI.NearbyLagrangian.Transport.flat_evolution_endpoint line 215