OAI/GroupTheory/PolycyclicRecognition/Algebra/FilteredBijection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Inverting a map whose error raises a finite filtration

The fixed-point correction terminates after the filtration length. This gives a concrete inverse for triangular polynomial translations.

  1. def OAI.PolycyclicRecognition.filteredNewton line 19
  2. theorem OAI.PolycyclicRecognition.filteredNewton_error_mem line 23
  3. theorem OAI.PolycyclicRecognition.filteredNewton_right_inverse line 41
  4. theorem OAI.PolycyclicRecognition.injective_of_raises_difference_filtration line 49
  5. theorem OAI.PolycyclicRecognition.bijective_of_raises_difference_filtration line 67
  6. theorem OAI.PolycyclicRecognition.continuous_filteredNewton line 78
  7. theorem OAI.PolycyclicRecognition.continuous_parametric_filteredNewton line 85
  8. def OAI.PolycyclicRecognition.homeomorphOfRaisesDifferenceFiltration line 92