Reduction of the potential inequality (6.2) to a finite check (Table 2)

For each interval [l, r] of the partition of (0, 2], the inequality 2Uρ(t) - V(t) ≤ M₀ on [l, r] follows from monotonicity of Uρ and V and one numerical inequality at the endpoints. The tail t ≥ 2 is handled by the elementary bound (6.8).

theorem Zeta5Irrational.aρ_one_lt_qm : aρ 1 < qm

theorem Zeta5Irrational.qp_lt_bρ_one : qp < bρ 1

theorem Zeta5Irrational.aρ_one_pos : 0 < aρ 1

theorem Zeta5Irrational.check_left {l r U V : ℝ} (hlr : l ≤ r) (hr : r ≤ aρ 1) (hU : Uρ l ≤ U) (hV : V ≤ Vfield r) (hnum : 2 * U - V ≤ M0) (t : ℝ) : l ≤ t → t ≤ r → 0 < t → 2 * Uρ t - Vfield t ≤ M0

Intervals to the left of a₁: Uρ nonincreasing, V nonincreasing.

theorem Zeta5Irrational.check_right {l r U V : ℝ} (hl : bρ 1 ≤ l) (hlr : l ≤ r) (hU : Uρ r ≤ U) (hV : V ≤ Vfield l) (hnum : 2 * U - V ≤ M0) (t : ℝ) : l ≤ t → t ≤ r → 0 < t → 2 * Uρ t - Vfield t ≤ M0

Intervals to the right of b₁: Uρ nondecreasing, V nondecreasing.

noncomputable def Zeta5Irrational.Uρmid : ℝ

The constant value of Uρ on [a₁, b₁].

Equations

• Zeta5Irrational.Uρmid = ∑ j ∈ Finset.Icc 1 16, Zeta5Irrational.cρ j * Real.log ((Zeta5Irrational.bρ j - Zeta5Irrational.aρ j) / 4)

theorem Zeta5Irrational.check_mid_left {U V : ℝ} (hU : Uρmid ≤ U) (hV : V ≤ Vfield qm) (hnum : 2 * U - V ≤ M0) (t : ℝ) : aρ 1 ≤ t → t ≤ qm → 0 < t → 2 * Uρ t - Vfield t ≤ M0

The interval [a₁, q₋].

theorem Zeta5Irrational.check_mid_right {U V : ℝ} (hU : Uρmid ≤ U) (hV : V ≤ Vfield qp) (hnum : 2 * U - V ≤ M0) (t : ℝ) : qp ≤ t → t ≤ bρ 1 → 0 < t → 2 * Uρ t - Vfield t ≤ M0

The interval [q₊, b₁].

theorem Zeta5Irrational.Vfield_ge_on_bracket {t : ℝ} (h1 : qm ≤ t) (h2 : t ≤ qp) : Real.log (1 + qm) - 6 * (3 / 40) * Real.log (qp + (3 / 40) ^ 2) - 2 + 12 * (3 / 40) + 2 * √qp * Pfun √qm ≤ Vfield t

The mixed lower bound for V on [q₋, q₊] (A.6): V(t) ≥ log(1+q₋) - 6α log(q₊ + α²) - 2 + 12α + 2√q₊ · P(√q₋).

theorem Zeta5Irrational.check_mid {U V : ℝ} (hU : Uρmid ≤ U) (hV : V ≤ Real.log (1 + qm) - 6 * (3 / 40) * Real.log (qp + (3 / 40) ^ 2) - 2 + 12 * (3 / 40) + 2 * √qp * Pfun √qm) (hnum : 2 * U - V ≤ M0) (t : ℝ) : qm ≤ t → t ≤ qp → 0 < t → 2 * Uρ t - Vfield t ≤ M0

The interval [q₋, q₊].

Wrappers for certified bounds

theorem Zeta5Irrational.log_le_of_ge_one {r U : ℝ} (hr : 1 ≤ r) (m : ℕ) (hU : 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

Upper bound for log r, r ≥ 1, from a numerical bound on the truncated series.

theorem Zeta5Irrational.log_ge_of_ge_one {r L : ℝ} (hr : 1 ≤ r) (m : ℕ) (hL : L ≤ 2 * ∑ k ∈ Finset.range m, 1 / (2 * ↑k + 1) * ((r - 1) / (r + 1)) ^ (2 * k + 1)) : L ≤ Real.log r

Lower bound for log r, r ≥ 1.

theorem Zeta5Irrational.log_le_of_le_one {w L : ℝ} (hw : 0 < w) (hw1 : w ≤ 1) (m : ℕ) (hL : L ≤ 2 * ∑ k ∈ Finset.range m, 1 / (2 * ↑k + 1) * ((w⁻¹ - 1) / (w⁻¹ + 1)) ^ (2 * k + 1)) : Real.log w ≤ -L

Upper bound for log w, 0 < w ≤ 1, via log w = - log w⁻¹.

theorem Zeta5Irrational.log_ge_of_le_one {w U : ℝ} (hw : 0 < w) (hw1 : w ≤ 1) (m : ℕ) (hU : 2 * ∑ k ∈ Finset.range m, 1 / (2 * ↑k + 1) * ((w⁻¹ - 1) / (w⁻¹ + 1)) ^ (2 * k + 1) + 2 * ((w⁻¹ - 1) / (w⁻¹ + 1)) ^ (2 * m + 1) / ((2 * ↑m + 1) * (1 - ((w⁻¹ - 1) / (w⁻¹ + 1)) ^ 2)) ≤ U) : -U ≤ Real.log w

Lower bound for log w, 0 < w ≤ 1.

theorem Zeta5Irrational.arctan_ge_of_series {z L : ℝ} (hz0 : 0 ≤ z) (hz1 : z < 1) (k : ℕ) (hL : L ≤ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * (z ^ (2 * i + 1) / (2 * ↑i + 1))) : L ≤ Real.arctan z

arctan z ≥ L from a truncated alternating series, 0 ≤ z < 1.

theorem Zeta5Irrational.arctan_le_of_series {z U : ℝ} (hz0 : 0 ≤ z) (hz1 : z < 1) (k : ℕ) (hU : ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * (z ^ (2 * i + 1) / (2 * ↑i + 1)) ≤ U) : Real.arctan z ≤ U

arctan z ≤ U from a truncated alternating series, 0 ≤ z < 1.

theorem Zeta5Irrational.arctan_ge_half {z hi L : ℝ} (hz : 0 ≤ z) (hhi : √(1 + z ^ 2) ≤ hi) (hL : L ≤ Real.arctan (z / (1 + hi))) : 2 * L ≤ Real.arctan z

Half-angle, lower bound: 2 L ≤ arctan z if L ≤ arctan (z / (1 + hi)) with √(1+z²) ≤ hi.

theorem Zeta5Irrational.arctan_le_half {z lo U : ℝ} (hz : 0 ≤ z) (hlo0 : 0 ≤ lo) (hlo : lo ≤ √(1 + z ^ 2)) (hU : Real.arctan (z / (1 + lo)) ≤ U) : Real.arctan z ≤ 2 * U

Half-angle, upper bound: arctan z ≤ 2 U if arctan (z / (1 + lo)) ≤ U with 0 ≤ lo ≤ √(1+z²).

theorem Zeta5Irrational.arctan_ge_inv {z U : ℝ} (hz : 0 < z) (hU : Real.arctan (1 / z) ≤ U) : Real.pi / 2 - U ≤ Real.arctan z

Inversion, lower bound: π/2 - U ≤ arctan z if arctan (1/z) ≤ U, z > 0.

theorem Zeta5Irrational.arctan_le_inv {z L : ℝ} (hz : 0 < z) (hL : L ≤ Real.arctan (1 / z)) : Real.arctan z ≤ Real.pi / 2 - L

Inversion, upper bound: arctan z ≤ π/2 - L if L ≤ arctan (1/z), z > 0.

theorem Zeta5Irrational.arctan_ge_of_le {x z L : ℝ} (hzx : z ≤ x) (hL : L ≤ Real.arctan z) : L ≤ Real.arctan x

Monotonicity transfer for arctan with a rational enclosure of the argument.

theorem Zeta5Irrational.arctan_le_of_ge {x z U : ℝ} (hxz : x ≤ z) (hU : Real.arctan z ≤ U) : Real.arctan x ≤ U

theorem Zeta5Irrational.Uρ_expand (x : ℝ) : Uρ x = cρ 1 * Uω (aρ 1) (bρ 1) x + cρ 2 * Uω (aρ 2) (bρ 2) x + cρ 3 * Uω (aρ 3) (bρ 3) x + cρ 4 * Uω (aρ 4) (bρ 4) x + cρ 5 * Uω (aρ 5) (bρ 5) x + cρ 6 * Uω (aρ 6) (bρ 6) x + cρ 7 * Uω (aρ 7) (bρ 7) x + cρ 8 * Uω (aρ 8) (bρ 8) x + cρ 9 * Uω (aρ 9) (bρ 9) x + cρ 10 * Uω (aρ 10) (bρ 10) x + cρ 11 * Uω (aρ 11) (bρ 11) x + cρ 12 * Uω (aρ 12) (bρ 12) x + cρ 13 * Uω (aρ 13) (bρ 13) x + cρ 14 * Uω (aρ 14) (bρ 14) x + cρ 15 * Uω (aρ 15) (bρ 15) x + cρ 16 * Uω (aρ 16) (bρ 16) x

The expanded form of Uρ.

theorem Zeta5Irrational.Uρmid_expand : Uρmid = cρ 1 * Real.log ((bρ 1 - aρ 1) / 4) + cρ 2 * Real.log ((bρ 2 - aρ 2) / 4) + cρ 3 * Real.log ((bρ 3 - aρ 3) / 4) + cρ 4 * Real.log ((bρ 4 - aρ 4) / 4) + cρ 5 * Real.log ((bρ 5 - aρ 5) / 4) + cρ 6 * Real.log ((bρ 6 - aρ 6) / 4) + cρ 7 * Real.log ((bρ 7 - aρ 7) / 4) + cρ 8 * Real.log ((bρ 8 - aρ 8) / 4) + cρ 9 * Real.log ((bρ 9 - aρ 9) / 4) + cρ 10 * Real.log ((bρ 10 - aρ 10) / 4) + cρ 11 * Real.log ((bρ 11 - aρ 11) / 4) + cρ 12 * Real.log ((bρ 12 - aρ 12) / 4) + cρ 13 * Real.log ((bρ 13 - aρ 13) / 4) + cρ 14 * Real.log ((bρ 14 - aρ 14) / 4) + cρ 15 * Real.log ((bρ 15 - aρ 15) / 4) + cρ 16 * Real.log ((bρ 16 - aρ 16) / 4)

The same expansion of Uρmid.

Binary range reduction for logarithms

theorem Zeta5Irrational.log_le_of_split_pos {r r' U : ℝ} (k : ℕ) (hr : r = 2 ^ k * r') (hr' : 0 < r') (hU : Real.log r' ≤ U) : Real.log r ≤ ↑k * Real.log 2 + U

theorem Zeta5Irrational.log_ge_of_split_pos {r r' L : ℝ} (k : ℕ) (hr : r = 2 ^ k * r') (hr' : 0 < r') (hL : L ≤ Real.log r') : ↑k * Real.log 2 + L ≤ Real.log r

theorem Zeta5Irrational.log_le_of_split_neg {r r' U : ℝ} (k : ℕ) (hr : r = r' / 2 ^ k) (hr' : 0 < r') (hU : Real.log r' ≤ U) : Real.log r ≤ U - ↑k * Real.log 2

theorem Zeta5Irrational.log_ge_of_split_neg {r r' L : ℝ} (k : ℕ) (hr : r = r' / 2 ^ k) (hr' : 0 < r') (hL : L ≤ Real.log r') : L - ↑k * Real.log 2 ≤ Real.log r