OAI/Geometry/SurfaceImmersion/Primitive/PrimitiveShiftedPowers.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The chosen slow scale also gives the finite two-jet input budget for the actual periodic primitive.

  1. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.slow_power_dominates_fast line 10
  2. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.primitive_shifted_budget line 18
  3. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.primitive_normal_threshold line 34