OAI/GroupTheory/PolycyclicRecognition/Analysis/PolynomialEnergyScales.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Small relative drops of polynomially bounded-below energy

A positive energy sequence with a polynomial lower bound cannot lose a fixed positive proportion at every sufficiently late step.

  1. theorem OAI.PolycyclicRecognition.tendsto_nat_add_one_pow_mul_geometric line 14
  2. theorem OAI.PolycyclicRecognition.exists_small_relative_energy_drop line 28