The tail integral ∫_{20}^{400} (x F(x) + 27/16)/x³ dx

On the grid t_i = 20 + i/3 (i ≤ 1140) the fractional parts {x} and {3x/40} are affine on each piece. With P = 74 g(1-g) - λ f(1-f) and C = (74/α) G₀(g) - λ G₀(f), G₀(v) = v(1-v)(2v-1)/6, we have P' = F + λ and C' = P - Pbar on each piece, and P, C are continuous across the breakpoints. Two integrations by parts on each piece and telescoping give ∑_i ∫_{t_i}^{t_{i+1}} (x F + 27/16)/x³ ≤ tailBound.

noncomputable def Zeta5Irrational.tT (i : ℕ) : ℝ

The grid.

Equations

• Zeta5Irrational.tT i = 20 + ↑i / 3

def Zeta5Irrational.qT (i : ℕ) : ℕ

Integer part of the left endpoint tT i of a tail interval.

Equations

• Zeta5Irrational.qT i = (60 + i) / 3

def Zeta5Irrational.qT' (i : ℕ) : ℕ

Integer part of 3 / 40 * tT i, used to fix the second fractional part.

Equations

• Zeta5Irrational.qT' i = (60 + i) / 40

noncomputable def Zeta5Irrational.FT (i : ℕ) (x : ℝ) : ℝ

F on the piece i.

Equations

• Zeta5Irrational.FT i x = 37 / 10 + 37 / 20 * (x - ↑(Zeta5Irrational.qT i)) - 111 / 10 * (3 / 40 * x - ↑(Zeta5Irrational.qT' i))

noncomputable def Zeta5Irrational.gT (i : ℕ) (x : ℝ) : ℝ

The tail majorant on piece i, including the additive error 27 / 16.

Equations

• Zeta5Irrational.gT i x = x * Zeta5Irrational.FT i x + 27 / 16

noncomputable def Zeta5Irrational.PT (i : ℕ) (x : ℝ) : ℝ

The quadratic oscillation contributed by the two fractional parts on tail piece i.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Zeta5Irrational.G0 (v : ℝ) : ℝ

Polynomial primitive of the centered quadratic v * (1 - v) - 1 / 6.

Equations

• Zeta5Irrational.G0 v = v * (1 - v) * (2 * v - 1) / 6

noncomputable def Zeta5Irrational.CT (i : ℕ) (x : ℝ) : ℝ

Primitive for the centered tail oscillation PT i - Pbar on piece i.

Equations

• Zeta5Irrational.CT i x = 74 * 40 / 3 * Zeta5Irrational.G0 (3 / 40 * x - ↑(Zeta5Irrational.qT' i)) - 37 / 40 * Zeta5Irrational.G0 (x - ↑(Zeta5Irrational.qT i))

noncomputable def Zeta5Irrational.Pbar : ℝ

Pbar = (74 - λ)/6.

Equations

• Zeta5Irrational.Pbar = 2923 / 240

The pieces

theorem Zeta5Irrational.tT_succ (i : ℕ) : tT (i + 1) = tT i + 1 / 3

theorem Zeta5Irrational.qT_le (i : ℕ) : ↑(qT i) ≤ tT i

theorem Zeta5Irrational.tT_succ_le (i : ℕ) : tT (i + 1) ≤ ↑(qT i) + 1

theorem Zeta5Irrational.qT'_le (i : ℕ) : ↑(qT' i) ≤ 3 / 40 * tT i

theorem Zeta5Irrational.tT_succ_le' (i : ℕ) : 3 / 40 * tT (i + 1) ≤ ↑(qT' i) + 1

theorem Zeta5Irrational.tT_pos (i : ℕ) : 20 ≤ tT i

theorem Zeta5Irrational.piece_coords {i : ℕ} {x : ℝ} (hx : x ∈ Set.Icc (tT i) (tT (i + 1))) : 0 ≤ x - ↑(qT i) ∧ x - ↑(qT i) ≤ 1 ∧ 0 ≤ 3 / 40 * x - ↑(qT' i) ∧ 3 / 40 * x - ↑(qT' i) ≤ 1

On the closed piece the local coordinates lie in [0, 1].

Derivatives

theorem Zeta5Irrational.hasDerivAt_PT (i : ℕ) (x : ℝ) : HasDerivAt (PT i) (FT i x + 37 / 40) x

theorem Zeta5Irrational.hasDerivAt_G0 (v : ℝ) : HasDerivAt G0 (v * (1 - v) - 1 / 6) v

theorem Zeta5Irrational.hasDerivAt_CT (i : ℕ) (x : ℝ) : HasDerivAt (CT i) (PT i x - Pbar) x

Continuity across breakpoints

theorem Zeta5Irrational.step3 (i : ℕ) : ↑(qT (i + 1)) = ↑(qT i) ∨ ↑(qT (i + 1)) = ↑(qT i) + 1 ∧ tT (i + 1) = ↑(qT (i + 1))

theorem Zeta5Irrational.step40 (i : ℕ) : ↑(qT' (i + 1)) = ↑(qT' i) ∨ ↑(qT' (i + 1)) = ↑(qT' i) + 1 ∧ 3 / 40 * tT (i + 1) = ↑(qT' (i + 1))

theorem Zeta5Irrational.PT_cont (i : ℕ) : PT i (tT (i + 1)) = PT (i + 1) (tT (i + 1))

theorem Zeta5Irrational.CT_cont (i : ℕ) : CT i (tT (i + 1)) = CT (i + 1) (tT (i + 1))

The antiderivative on a piece

noncomputable def Zeta5Irrational.PhiT (i : ℕ) (x : ℝ) : ℝ

Φ_i(x) = P/x² + 2C/x³ - Pbar/x² + λ/x - (27/32)/x².

Equations

• Zeta5Irrational.PhiT i x = Zeta5Irrational.PT i x / x ^ 2 + 2 * Zeta5Irrational.CT i x / x ^ 3 - Zeta5Irrational.Pbar / x ^ 2 + 37 / 40 / x - 27 / 32 / x ^ 2

theorem Zeta5Irrational.hasDerivAt_PhiT (i : ℕ) {x : ℝ} (hx : 0 < x) : HasDerivAt (PhiT i) (gT i x / x ^ 3 - 6 * CT i x / x ^ 4) x

theorem Zeta5Irrational.continuous_gT (i : ℕ) : Continuous (gT i)

theorem Zeta5Irrational.continuous_CT (i : ℕ) : Continuous (CT i)

theorem Zeta5Irrational.continuousOn_div_pow {f : ℝ → ℝ} (hf : Continuous f) (k : ℕ) {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : ContinuousOn (fun (x : ℝ) => f x / x ^ k) (Set.uIcc a b)

theorem Zeta5Irrational.abs_G0_le {v : ℝ} (h0 : 0 ≤ v) (h1 : v ≤ 1) : |G0 v| ≤ 1 / 60

theorem Zeta5Irrational.abs_CT_le {i : ℕ} {x : ℝ} (hx : x ∈ Set.Icc (tT i) (tT (i + 1))) : |CT i x| ≤ 17

theorem Zeta5Irrational.piece_bound (i : ℕ) : ∫ (x : ℝ) in tT i..tT (i + 1), gT i x / x ^ 3 ≤ PhiT i (tT (i + 1)) - PhiT i (tT i) + 34 * (1 / tT i ^ 3 - 1 / tT (i + 1) ^ 3)

One piece.

theorem Zeta5Irrational.PhiT_cont (i : ℕ) : PhiT i (tT (i + 1)) = PhiT (i + 1) (tT (i + 1))

theorem Zeta5Irrational.tele_phi (N : ℕ) : ∑ i ∈ Finset.range N, (PhiT i (tT (i + 1)) - PhiT i (tT i)) = PhiT N (tT N) - PhiT 0 (tT 0)

theorem Zeta5Irrational.tele_cube (N : ℕ) : ∑ i ∈ Finset.range N, 34 * (1 / tT i ^ 3 - 1 / tT (i + 1) ^ 3) = 34 * (1 / tT 0 ^ 3 - 1 / tT N ^ 3)

theorem Zeta5Irrational.tail_sum_le : ∑ i ∈ Finset.range 1140, ∫ (x : ℝ) in tT i..tT (i + 1), gT i x / x ^ 3 ≤ -6843153 / 128000000

The tail sum: ∑_i ∫_{t_i}^{t_{i+1}} g_i/x³ ≤ -6843153/128000000 ≈ -0.05346.