OAI/GroupTheory/PolycyclicRecognition/Analysis/SequencePolynomialImage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact image-volume witnesses for arbitrary measurable parameters

The domain can have more coordinates than the range. The scalar polynomial is an actual derivative minor. Remez, inner regularity, Fubini, and the quantitative injective patch estimate provide the compact image witnesses.

  1. theorem OAI.PolycyclicRecognition.exists_subexponential_polynomial_image_sequence line 22