OAI/Geometry/SurfaceImmersion/Correction/UniformFreeModeConstants.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit free-mode constants, independent of both short scales and of the perturbation size. These constants are used before selecting scales.

  1. def OAI.ClosedSurfaceR4.SmallModes.freeModeBudget line 14
  2. lemma OAI.ClosedSurfaceR4.SmallModes.freeModeBudget_nonneg line 21
  3. theorem OAI.ClosedSurfaceR4.SmallModes.freeModeBudget_bound line 31
  4. theorem OAI.ClosedSurfaceR4.SmallModes.freeModeBudget_size line 50