Generic tools for the rational point checks of ρ_{a₋} and ℓ(a).

• lser_le_log: log z ≥ 2(t + t³/3 + t⁵/5 + t⁷/7), t = (z−1)/(z+1), for z ≥ 1 (partial sum of the nonnegative series log(1+t) − log(1−t) = Σ 2t^(2k+1)/(2k+1), Mathlib hasSum_log_sub_log_of_abs_lt_one).
• log_ge, log_ge', log_le: argument reduction by 2^m with Mathlib's log_two_gt_d9, log_two_lt_d9.
• G_ge, G_le: Gfun is increasing in s = √(a²−x²) and decreasing in U = √(c²+a²).
• rho_ge_of: one point R ≤ ρ_{a₋}(x) from rational brackets of the square roots and one log lower bound. Written from scratch.

noncomputable def Zeta32.Fstar.B2.lser (t : ℝ) : ℝ

Partial sum 2(t + t³/3 + t⁵/5 + t⁷/7) of log((1+t)/(1−t)).

Equations

• Zeta32.Fstar.B2.lser t = 2 * (t + t ^ 3 / 3 + t ^ 5 / 5 + t ^ 7 / 7)

theorem Zeta32.Fstar.B2.lser_le_log {z : ℝ} (hz : 1 ≤ z) : lser ((z - 1) / (z + 1)) ≤ Real.log z

theorem Zeta32.Fstar.B2.log_ge (y : ℝ) (m : ℕ) (h : 2 ^ m ≤ y) : ↑m * (6931471803 / 10 ^ 10) + lser ((y / 2 ^ m - 1) / (y / 2 ^ m + 1)) ≤ Real.log y

Lower bound log y ≥ m·log 2 + lser(...) for y ≥ 2^m.

theorem Zeta32.Fstar.B2.log_ge' (y : ℝ) (m : ℕ) (h : 1 ≤ 2 ^ m * y) : -(↑m * (6931471808 / 10 ^ 10)) + lser ((2 ^ m * y - 1) / (2 ^ m * y + 1)) ≤ Real.log y

Lower bound log y ≥ −m·log 2 + lser(...) for 2^m·y ≥ 1.

theorem Zeta32.Fstar.B2.log_le (y : ℝ) (m : ℕ) (hy : 0 < y) (h : y ≤ 2 ^ m) : Real.log y ≤ ↑m * (6931471808 / 10 ^ 10) - lser ((2 ^ m / y - 1) / (2 ^ m / y + 1))

Upper bound log y ≤ m·log 2 − lser(...) for 0 < y ≤ 2^m.

theorem Zeta32.Fstar.B2.le_sqrt_of_sq_le {l y : ℝ} (hl : 0 ≤ l) (h : l ^ 2 ≤ y) : l ≤ √y

theorem Zeta32.Fstar.B2.sqrt_le_of_le_sq {u y : ℝ} (hu : 0 ≤ u) (h : y ≤ u ^ 2) : √y ≤ u

theorem Zeta32.Fstar.B2.G_ge {a c x sl Uh : ℝ} (hx : 0 < x) (hxa : x ≤ a) (hsl0 : 0 ≤ sl) (hsl : sl ≤ √(a ^ 2 - x ^ 2)) (hU : √(c ^ 2 + a ^ 2) ≤ Uh) : Real.log ((Uh + sl) / (Uh - sl)) ≤ Gfun a c x

Gfun from below: smaller s, larger U.

theorem Zeta32.Fstar.B2.G_le {a c x sh Ul : ℝ} (hsh : √(a ^ 2 - x ^ 2) ≤ sh) (hU : Ul ≤ √(c ^ 2 + a ^ 2)) (hshU : sh < Ul) : Gfun a c x ≤ Real.log ((Ul + sh) / (Ul - sh))

Gfun from above: larger s, smaller U.

theorem Zeta32.Fstar.B2.rho_ge_of {x sl sh U1 U5 P R : ℝ} (hx : 0 < x) (hxa : x ≤ aMinus) (hsl0 : 0 ≤ sl) (hsl : sl ^ 2 ≤ aMinus ^ 2 - x ^ 2) (hsh0 : 0 ≤ sh) (hsh : aMinus ^ 2 - x ^ 2 ≤ sh ^ 2) (hU10 : 0 ≤ U1) (hU1 : 1 + aMinus ^ 2 ≤ U1 ^ 2) (hU50 : 0 ≤ U5) (hU5 : U5 ^ 2 ≤ 25 + aMinus ^ 2) (hshU5 : sh < U5) (hP0 : 0 < P) (hP : P ≤ (aMinus + sl) / (aMinus - sl) * ((U1 + sl) / (U1 - sl)) ^ 4 / ((U5 + sh) / (U5 - sh))) (hR0 : 0 ≤ R) (hR : 12 * (31416 / 10000) * R ≤ Real.log P) : R ≤ rhoA aMinus x

One point of ρ_{a₋}: ρ = (G₀ + 4G₁ − G₅)/(12π), each G bracketed through rational s, U, the three logs merged into log P.