OAI/Geometry/SurfaceImmersion/Correction/PerturbedFreeMode.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite correction of an actual supported free normal seed in the presence of the polynomial differential perturbation.

  1. def OAI.ClosedSurfaceR4.SmallModes.perturbedFreeMode line 18
  2. lemma OAI.ClosedSurfaceR4.SmallModes.perturbed_initial_free_bound line 25