OAI/Geometry/SurfaceImmersion/Primitive/PrimitiveInitialFamily.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The concrete starting family for the finite primitive iteration. At amplitude z^(1/4), both its C2 displacement and its normalized mean defect are bounded by fixed multiples of z^(1/2).

  1. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.initial_amplitude_square line 15
  2. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.initial_error_quotient line 20
  3. theorem OAI.ClosedSurfaceR4.PrimitiveRealization.primitive_initial_family line 28