theorem G67ElementaryIntegral.upper_reciprocal_lower {s : ℝ} (hs : 0 < s) : 2 * Real.exp Real.eulerMascheroniConstant / s ≤ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F s

The constructed upper delay function dominates its initial reciprocal globally.

theorem G67ElementaryIntegral.lower_log {s : ℝ} (hs : 2 ≤ s) : 2 * Real.exp Real.eulerMascheroniConstant * Real.log (s - 1) / s ≤ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f s

The elementary logarithmic lower bound follows from the actual delay recurrence. It holds on the whole half-line, hence in particular up to 37/8.

noncomputable def G67ElementaryIntegral.elementaryKernel (x : ℝ × ℝ) : ℝ

The literal explicit logarithmic kernel, not a replacement definition of C67.

Equations

• G67ElementaryIntegral.elementaryKernel x = max 0 (Real.log ((1 / 2 - x.1 - x.2 - 4 / 53) / (4 / 53)) / (1 / 2 - x.1 - x.2))

theorem G67ElementaryIntegral.domain_bounds {u v : ℝ} (hu : u ∈ Set.Icc (4 / 53) (4 / 33)) (hv : v ∈ Set.Icc (4 / 53) (3 / 11)) : 0 < u ∧ 0 < v ∧ 0 < 1 / 2 - u - v ∧ 0 < (1 / 2 - u - v - 4 / 53) / (4 / 53) ∧ (1 / 2 - u - v) / (4 / 53) ≤ 37 / 8

Geometry of the full union, including every point of the square diagonal.

theorem G67ElementaryIntegral.kernel_lower {u v : ℝ} (hu : u ∈ Set.Icc (4 / 53) (4 / 33)) (hv : v ∈ Set.Icc (4 / 53) (3 / 11)) : 2 * Real.exp Real.eulerMascheroniConstant * (4 / 53) * elementaryKernel (u, v) ≤ LiLiuGoldbachIdealPairKernel.kernel 0 (u, v)

Pointwise comparison with the actual zero-truncation JR kernel.