Actual JR lower function: global real-domain Lipschitz and endpoint control.

theorem MathlibNt.SieveTheory.LiLiuGoldbachJRLowerLipschitz.lower_monotone : Monotone JurkatRichert1965ChenGammaOneQOne.jr1965f

The zero extension below two makes the actual lower function globally monotone.

theorem MathlibNt.SieveTheory.LiLiuGoldbachJRLowerLipschitz.lower_sub_le_half_constant_mul {x y : ℝ} (hxy : x ≤ y) : JurkatRichert1965ChenGammaOneQOne.jr1965f y - JurkatRichert1965ChenGammaOneQOne.jr1965f x ≤ JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant / 2 * (y - x)

Ordered global increment bound, including intervals crossing two.

theorem MathlibNt.SieveTheory.LiLiuGoldbachJRLowerLipschitz.lower_abs_sub_le (x y : ℝ) : |JurkatRichert1965ChenGammaOneQOne.jr1965f x - JurkatRichert1965ChenGammaOneQOne.jr1965f y| ≤ JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant / 2 * |x - y|

Global Lipschitz estimate: neither input is assumed positive.

theorem MathlibNt.SieveTheory.LiLiuGoldbachJRLowerLipschitz.lower_le_add_abs (x y : ℝ) : JurkatRichert1965ChenGammaOneQOne.jr1965f y ≤ JurkatRichert1965ChenGammaOneQOne.jr1965f x + JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant / 2 * |x - y|

One-sided transport form for downstream nonnegative-counting branches.

theorem MathlibNt.SieveTheory.LiLiuGoldbachJRLowerLipschitz.lower_le_near_two {x y η : ℝ} (hx : x ≤ 2) (hclose : |x - y| < η) : JurkatRichert1965ChenGammaOneQOne.jr1965f y ≤ JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant / 2 * η

If the source is at or below two, the target may lie on either side of two.