OAI/NumberTheory/CubicMoment/Estimates/FixedScalePowers.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Fixed dilations preserve every strict exponent margin used by the finite output partition.

  1. lemma OAI.CubicFirstMoment.eventually_const_mul_rpow_le line 11
  2. lemma OAI.CubicFirstMoment.eventually_rpow_le_const_mul line 19
  3. lemma OAI.CubicFirstMoment.eventually_scaled_rpow_le line 26
  4. lemma OAI.CubicFirstMoment.eventually_rpow_le_scaled line 31
  5. lemma OAI.CubicFirstMoment.eventually_scaled_power_window line 37
  6. lemma OAI.CubicFirstMoment.eventually_scaled_coordinate_lower line 43
  7. structure OAI.CubicFirstMoment.FixedScaleMomentBounds line 52
  8. lemma OAI.CubicFirstMoment.eventually_fixed_scale_moment_bounds line 63