Certified rational bounds for `log`, `arctan` and `sqrt` #

Tools for the numerical verification of the potential inequality (6.2) (Lemma 6.1):

log_le_artanh : upper bound for log r, r ≥ 1, by a partial sum of the artanh series plus an explicit geometric tail (complementing log_ge_artanh);
arctan_ge_partial / arctan_le_partial : two-sided bounds for arctan x, 0 ≤ x < 1, by partial sums of the alternating series;
arctan_eq_two_mul_arctan : the half-angle reduction arctan x = 2 arctan (x / (1 + √(1+x²)));
sqrt_le_of_sq_le, le_sqrt_of_sq_le : rational enclosures of square roots.

theorem Zeta5Irrational.log_le_artanh {r : ℝ} (hr : 1 ≤ r) (m : ℕ) :

Real.log r ≤ 2 * ∑ k ∈ Finset.range m, 1 / (2 * ↑k + 1) * ((r - 1) / (r + 1)) ^ (2 * k + 1) + 2 * ((r - 1) / (r + 1)) ^ (2 * m + 1) / ((2 * ↑m + 1) * (1 - ((r - 1) / (r + 1)) ^ 2))

Upper bound for log r, r ≥ 1: partial sum plus the tail 2 z^(2m+1) / ((2m+1)(1 - z²)).

theorem Zeta5Irrational.arctan_ge_partial {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x < 1) (k : ℕ) :

∑ i ∈ Finset.range (2 * k), (-1) ^ i * (x ^ (2 * i + 1) / (2 * ↑i + 1)) ≤ Real.arctan x

Lower bound arctan x ≥ ∑_{i < 2k} (-1)^i x^(2i+1)/(2i+1) for 0 ≤ x < 1.

theorem Zeta5Irrational.arctan_le_partial {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x < 1) (k : ℕ) :

Real.arctan x ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * (x ^ (2 * i + 1) / (2 * ↑i + 1))

Upper bound arctan x ≤ ∑_{i < 2k+1} (-1)^i x^(2i+1)/(2i+1) for 0 ≤ x < 1.

The half-angle reduction arctan x = 2 arctan (x / (1 + √(1 + x²))) for x ≥ 0.

theorem Zeta5Irrational.sqrt_le_of_sq_le {q u : ℝ} (hu : 0 ≤ u) (h : q ≤ u ^ 2) :

Rational enclosure of a square root: √q ≤ u if q ≤ u², 0 ≤ u.

theorem Zeta5Irrational.le_sqrt_of_sq_le {q l : ℝ} (_hl : 0 ≤ l) (h : l ^ 2 ≤ q) :

Rational enclosure of a square root: l ≤ √q if l² ≤ q, 0 ≤ l.

Documentation