Rational certificates for finite analytic series

The table bounds use only rational inputs. Check their finite sums in ℚ, then transport one inequality to ℝ, avoiding a separate normalization proof for every real operation.

theorem Zeta5Irrational.log_le_of_ge_one_rat {r U : ℚ} (m : ℕ) (certificate : 1 ≤ 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)) ≤ U) : Real.log ↑r ≤ ↑U

A rational upper certificate for the logarithm series and its geometric tail.

theorem Zeta5Irrational.log_ge_of_ge_one_rat {r L : ℚ} (m : ℕ) (certificate : 1 ≤ r ∧ L ≤ 2 * ∑ k ∈ Finset.range m, 1 / (2 * ↑k + 1) * ((r - 1) / (r + 1)) ^ (2 * k + 1)) : ↑L ≤ Real.log ↑r

A rational lower certificate for the logarithm series.

theorem Zeta5Irrational.arctan_ge_of_series_rat {z L : ℚ} (k : ℕ) (certificate : 0 ≤ z ∧ z < 1 ∧ L ≤ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * (z ^ (2 * i + 1) / (2 * ↑i + 1))) : ↑L ≤ Real.arctan ↑z

A rational lower certificate for the alternating arctangent series.

theorem Zeta5Irrational.arctan_le_of_series_rat {z U : ℚ} (k : ℕ) (certificate : 0 ≤ z ∧ z < 1 ∧ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * (z ^ (2 * i + 1) / (2 * ↑i + 1)) ≤ U) : Real.arctan ↑z ≤ ↑U

A rational upper certificate for the alternating arctangent series.