Four integrations by parts: `∫₀^∞ g F₄ = ∫₀^∞ g₄ F₀` #

Uniform bounds |F_m(y)| ≤ c_m (1+2πy)^{m+1} / (2π y^{m+1} e^{2πy}) and |g_j(y)| ≤ c_j y^{5-j}/a² give integrability of the products and vanishing boundary terms at 0⁺ and ∞.

Bounds for `F_m` #

source

theorem Zeta5Irrational.qe_sub_one_ge {y : ℝ} :

2 * Real.pi * y ≤ qe y - 1

source

theorem Zeta5Irrational.one_div_qe_sub_one_le {y : ℝ} (hy : 0 < y) :

1 / (qe y - 1) ≤ (1 + 2 * Real.pi * y) / (2 * Real.pi * y * qe y)

source

theorem Zeta5Irrational.F_bound_aux {y : ℝ} (hy : 0 < y) (m : ℕ) {N c : ℝ} (hN : 0 ≤ N) (hNc : N ≤ (2 * Real.pi) ^ m * c * qe y ^ m) :

N / (qe y - 1) ^ (m + 1) ≤ c * (1 + 2 * Real.pi * y) ^ (m + 1) / (2 * Real.pi * y ^ (m + 1) * qe y)

Generic estimate N / (q-1)^(m+1) ≤ c (1+2πy)^(m+1) / (2π y^(m+1) q) when N ≤ (2π)^m c q^m.

source

theorem Zeta5Irrational.abs_F0_le {y : ℝ} (hy : 0 < y) :

|F0 y| ≤ 1 * (1 + 2 * Real.pi * y) ^ (0 + 1) / (2 * Real.pi * y ^ (0 + 1) * qe y)

source

theorem Zeta5Irrational.abs_F1_le {y : ℝ} (hy : 0 < y) :

|F1 y| ≤ 1 * (1 + 2 * Real.pi * y) ^ (1 + 1) / (2 * Real.pi * y ^ (1 + 1) * qe y)

source

theorem Zeta5Irrational.abs_F2_le {y : ℝ} (hy : 0 < y) :

|F2 y| ≤ 2 * (1 + 2 * Real.pi * y) ^ (2 + 1) / (2 * Real.pi * y ^ (2 + 1) * qe y)

source

theorem Zeta5Irrational.abs_F3_le {y : ℝ} (hy : 0 < y) :

|F3 y| ≤ 6 * (1 + 2 * Real.pi * y) ^ (3 + 1) / (2 * Real.pi * y ^ (3 + 1) * qe y)

source

theorem Zeta5Irrational.abs_F4_le {y : ℝ} (hy : 0 < y) :

|F4 y| ≤ 24 * (1 + 2 * Real.pi * y) ^ (4 + 1) / (2 * Real.pi * y ^ (4 + 1) * qe y)

Bounds for `g_j` #

source

theorem Zeta5Irrational.abs_g0_le {a : ℝ} (ha : 0 < a) {y : ℝ} (hy : 0 ≤ y) :

|g0 a y| ≤ 1 / 12 * y ^ 5 / a ^ 2

source

theorem Zeta5Irrational.abs_g1_le {a : ℝ} (ha : 0 < a) {y : ℝ} (_hy : 0 ≤ y) :

|g1 a y| ≤ 5 / 12 * y ^ 4 / a ^ 2

source

theorem Zeta5Irrational.abs_g2_le {a : ℝ} (ha : 0 < a) {y : ℝ} (hy : 0 ≤ y) :

|g2 a y| ≤ 10 / 6 * y ^ 3 / a ^ 2

source

theorem Zeta5Irrational.abs_g3_le {a : ℝ} (ha : 0 < a) {y : ℝ} (_hy : 0 ≤ y) :

|g3 a y| ≤ 5 * y ^ 2 / a ^ 2

source

theorem Zeta5Irrational.g4_eq_mul_h4 (a y : ℝ) :

g4 a y = y * h4 a y

source

theorem Zeta5Irrational.abs_g4_le' {a : ℝ} (ha : 0 < a) {y : ℝ} (hy : 0 ≤ y) :

|g4 a y| ≤ 20 * y / a ^ 2

Product bounds #

source

theorem Zeta5Irrational.prod_bound_aux {a y : ℝ} (ha : 0 < a) (hy : 0 < y) {G Fv c d : ℝ} {m e : ℕ} (hG : |G| ≤ c * y ^ (m + 1 + e) / a ^ 2) (hF : |Fv| ≤ d * (1 + 2 * Real.pi * y) ^ (m + 1) / (2 * Real.pi * y ^ (m + 1) * qe y)) (hc : 0 ≤ c) (_hd : 0 ≤ d) (hcd : c * d ≤ 8 * Real.pi) (hm : m + 1 ≤ 5) :

|G * Fv| ≤ 4 * y ^ e * (1 + 2 * Real.pi * y) ^ 5 / (a ^ 2 * qe y)

|G F| ≤ 4 y^e (1+2πy)^5 / (a² q) from |G| ≤ c y^(m+1+e)/a², |F| ≤ d (1+2πy)^(m+1)/(2π y^(m+1) q), c d ≤ 8π, m + 1 ≤ 5.

source

theorem Zeta5Irrational.abs_g0F4_le {a : ℝ} (ha : 0 < a) {y : ℝ} (hy : 0 < y) :

|g0 a y * F4 y| ≤ 4 * y ^ 0 * (1 + 2 * Real.pi * y) ^ 5 / (a ^ 2 * qe y)

source

theorem Zeta5Irrational.abs_g1F3_le {a : ℝ} (ha : 0 < a) {y : ℝ} (hy : 0 < y) :

|g1 a y * F3 y| ≤ 4 * y ^ 0 * (1 + 2 * Real.pi * y) ^ 5 / (a ^ 2 * qe y)

source

theorem Zeta5Irrational.abs_g2F2_le {a : ℝ} (ha : 0 < a) {y : ℝ} (hy : 0 < y) :

|g2 a y * F2 y| ≤ 4 * y ^ 0 * (1 + 2 * Real.pi * y) ^ 5 / (a ^ 2 * qe y)

source

theorem Zeta5Irrational.abs_g3F1_le {a : ℝ} (ha : 0 < a) {y : ℝ} (hy : 0 < y) :

|g3 a y * F1 y| ≤ 4 * y ^ 0 * (1 + 2 * Real.pi * y) ^ 5 / (a ^ 2 * qe y)

source

theorem Zeta5Irrational.abs_g4F0_le {a : ℝ} (ha : 0 < a) {y : ℝ} (hy : 0 < y) :

|g4 a y * F0 y| ≤ 4 * y ^ 0 * (1 + 2 * Real.pi * y) ^ 5 / (a ^ 2 * qe y)

source

theorem Zeta5Irrational.abs_g0F3_le {a : ℝ} (ha : 0 < a) {y : ℝ} (hy : 0 < y) :

|g0 a y * F3 y| ≤ 4 * y ^ 1 * (1 + 2 * Real.pi * y) ^ 5 / (a ^ 2 * qe y)

source

theorem Zeta5Irrational.abs_g1F2_le {a : ℝ} (ha : 0 < a) {y : ℝ} (hy : 0 < y) :

|g1 a y * F2 y| ≤ 4 * y ^ 1 * (1 + 2 * Real.pi * y) ^ 5 / (a ^ 2 * qe y)

source

theorem Zeta5Irrational.abs_g2F1_le {a : ℝ} (ha : 0 < a) {y : ℝ} (hy : 0 < y) :

|g2 a y * F1 y| ≤ 4 * y ^ 1 * (1 + 2 * Real.pi * y) ^ 5 / (a ^ 2 * qe y)

source

theorem Zeta5Irrational.abs_g3F0_le {a : ℝ} (ha : 0 < a) {y : ℝ} (hy : 0 < y) :

|g3 a y * F0 y| ≤ 4 * y ^ 1 * (1 + 2 * Real.pi * y) ^ 5 / (a ^ 2 * qe y)

`(1 + x)^5 e^{-x} ≤ C e^{-x/2}` #

source

theorem Zeta5Irrational.poly_exp_bound {x : ℝ} (hx : 0 ≤ x) :

(1 + x) ^ 5 * Real.exp (-x) ≤ 122912 * Real.exp (-(x / 2))

source

theorem Zeta5Irrational.bound_exp {a y : ℝ} (ha : 0 < a) (hy : 0 < y) (e : ℕ) :

4 * y ^ e * (1 + 2 * Real.pi * y) ^ 5 / (a ^ 2 * qe y) ≤ 4 * 122912 / a ^ 2 * (y ^ e * Real.exp (-(Real.pi * y)))

Continuity, integrability, limits #

source

theorem Zeta5Irrational.continuous_qe :

Continuous qe

source

theorem Zeta5Irrational.qe_sub_one_ne {y : ℝ} (hy : y ∈ Set.Ioi 0) :

qe y - 1 ≠ 0

source

theorem Zeta5Irrational.continuousOn_F0 :

ContinuousOn F0 (Set.Ioi 0)

source

theorem Zeta5Irrational.continuousOn_F1 :

ContinuousOn F1 (Set.Ioi 0)

source

theorem Zeta5Irrational.continuousOn_F2 :

ContinuousOn F2 (Set.Ioi 0)

source

theorem Zeta5Irrational.continuousOn_F3 :

ContinuousOn F3 (Set.Ioi 0)

source

theorem Zeta5Irrational.continuousOn_F4 :

ContinuousOn F4 (Set.Ioi 0)

source

theorem Zeta5Irrational.continuous_g0 {a : ℝ} (ha : 0 < a) :

Continuous (g0 a)

source

theorem Zeta5Irrational.continuous_g1 {a : ℝ} (ha : 0 < a) :

Continuous (g1 a)

source

theorem Zeta5Irrational.continuous_g2 {a : ℝ} (ha : 0 < a) :

Continuous (g2 a)

source

theorem Zeta5Irrational.continuous_g3 {a : ℝ} (ha : 0 < a) :

Continuous (g3 a)

source

theorem Zeta5Irrational.integrableOn_of_prod_bound {a : ℝ} (ha : 0 < a) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Ioi 0)) (hb : ∀ (y : ℝ), 0 < y → |f y| ≤ 4 * y ^ 0 * (1 + 2 * Real.pi * y) ^ 5 / (a ^ 2 * qe y)) :

MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume

Integrability on (0, ∞) of a product bounded by 4 y^0 (1+2πy)^5/(a² q).

source

theorem Zeta5Irrational.tendsto_of_prod_bound {a : ℝ} (ha : 0 < a) {f : ℝ → ℝ} (hb : ∀ (y : ℝ), 0 < y → |f y| ≤ 4 * y ^ 1 * (1 + 2 * Real.pi * y) ^ 5 / (a ^ 2 * qe y)) :