OAI/GroupTheory/PolycyclicRecognition/Geometry/SmoothPolynomialFamilyImage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Measurable images in a compact smooth polynomial family

Smoothness supplies all local differential bounds. The polynomial formulas supply the actual minor and its fixed degree. Only scalar Remez is external.

  1. theorem OAI.PolycyclicRecognition.contDiff_finAppend line 21
  2. theorem OAI.PolycyclicRecognition.compact_smooth_polynomial_family_image line 31