OAI/Geometry/SurfaceImmersion/Whitney/ShiftedRotationFilling.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A compact explicit filling of the frame for two equal-index zeros.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shiftedDoubleFrame line 13
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.filledShiftedRotation line 16
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.filledShiftedRotation_smooth line 20
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.norm_large_square_sum_radius line 31
  5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_shifted_double_filling_radius line 48
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.norm_large_square_sum line 104
  7. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_shifted_double_filling line 107