Uniform changes of sieve coordinate

The actual delay equations give a derivative bound of order 1 / s on [s, ∞). Thus multiplicative coordinate changes have a bound independent of the (unbounded) coordinate. The endpoint s = 2 needs only continuity.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoordinateShift.delayConstant_pos : 0 < JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoordinateShift.upper_sub_le_relative_length {s t : ℝ} (hs : 2 ≤ s) (hst : s ≤ t) : JurkatRichert1965ChenGammaOneQOne.jr1965F s - JurkatRichert1965ChenGammaOneQOne.jr1965F t ≤ JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant / s * (t - s)

The upper function changes at most by the delay constant times relative length.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoordinateShift.lower_sub_le_relative_length {s t : ℝ} (hs : 2 ≤ s) (hst : s ≤ t) : JurkatRichert1965ChenGammaOneQOne.jr1965f t - JurkatRichert1965ChenGammaOneQOne.jr1965f s ≤ JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant / s * (t - s)

The lower function obeys the same relative-length estimate.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoordinateShift.scale_bounds {ε : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8) : 1 ≤ 1 + ε + ε ^ 9 ∧ 1 + ε + ε ^ 9 ≤ 1 + 2 * ε ∧ 2 * (1 + ε + ε ^ 9) < 3

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoordinateShift.abs_shifts_le {ε s : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8) (hs : 2 ≤ s) : |JurkatRichert1965ChenGammaOneQOne.jr1965F s - JurkatRichert1965ChenGammaOneQOne.jr1965F ((1 + ε + ε ^ 9) * s)| ≤ 2 * JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant * ε ∧ |JurkatRichert1965ChenGammaOneQOne.jr1965f ((1 + ε + ε ^ 9) * s) - JurkatRichert1965ChenGammaOneQOne.jr1965f s| ≤ 2 * JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant * ε

Both absolute shifts are uniform over the entire source range s ≥ 2.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoordinateShift.exists_uniform_coordinate_shift : ∃ C > 0, ∀ (ε : ℝ), 0 < ε → ε < 1 / 8 → ∀ (s : ℝ), 2 ≤ s → JurkatRichert1965ChenGammaOneQOne.jr1965F s ≤ JurkatRichert1965ChenGammaOneQOne.jr1965F ((1 + ε + ε ^ 9) * s) + C * ε ∧ JurkatRichert1965ChenGammaOneQOne.jr1965f ((1 + ε + ε ^ 9) * s) ≤ JurkatRichert1965ChenGammaOneQOne.jr1965f s + C * ε

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoordinateShift.lower_edge_le {ε sQ : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8) (hsQ : 2 ≤ sQ) (hsQc : sQ ≤ 2 * (1 + ε + ε ^ 9)) : JurkatRichert1965ChenGammaOneQOne.jr1965f sQ ≤ 2 * JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant * ε

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoordinateShift.upper_edge_exact {c sQ : ℝ} (_hsQ : 2 ≤ sQ) (hsQc : sQ ≤ 2 * c) (hc3 : 2 * c < 3) : JurkatRichert1965ChenGammaOneQOne.jr1965F 2 * (2 * c / sQ) = JurkatRichert1965ChenGammaOneQOne.jr1965F sQ * c

Exact cancellation of the edge upper main term against the logarithm ratio.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoordinateShift.upper_edge_exact_epsilon {ε sQ : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8) (hsQ : 2 ≤ sQ) (hsQc : sQ ≤ 2 * (1 + ε + ε ^ 9)) : JurkatRichert1965ChenGammaOneQOne.jr1965F 2 * (2 * (1 + ε + ε ^ 9) / sQ) = JurkatRichert1965ChenGammaOneQOne.jr1965F sQ * (1 + ε + ε ^ 9)