OAI/NumberTheory/JointDickman/Amplification/AuxiliaryPowerSeparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Strict power gaps absorb the fixed endpoint dilations

  1. lemma OAI.JointDickman.eventually_scaled_power_lt line 10