OAI/Geometry/SurfaceImmersion/Primitive/PrimitiveSlowErrorProfiles.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform all-order power profiles for the two primitive error terms.

  1. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.normalized_slow_error_profile line 9
  2. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.slow_parameter_bound_of_exponents line 31