OAI/Geometry/SurfaceImmersion/Correction/SupportedFreeLinearity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The free seed and its finite perturbed correction are actual linear maps.

  1. def OAI.ClosedSurfaceR4.SmallModes.initialFreeLM line 15
  2. def OAI.ClosedSurfaceR4.SmallModes.perturbedFreeLM line 51
  3. lemma OAI.ClosedSurfaceR4.SmallModes.perturbedFreeLM_apply line 59