OAI/Geometry/SurfaceImmersion/Atlas/PhaseDenominatorNeighborhood.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A compact-support denominator bound extends to an open phase domain with a specified factor of two. The domain may depend on the immersion; the numerical bounds do not.

  1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.continuousAt_phaseNormal line 14
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.eventually_gram_reciprocal_bound line 30
  3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.eventually_normal_reciprocal_bound line 39
  4. theorem OAI.ClosedSurfaceR4.PhaseGeometry.phase_denominator_neighborhood line 51