The weight w of (2.10)

w(y) = (2π)⁴ y⁵ / 12 · ∑_{ℓ ≥ 1} ℓ⁴ e^{-2πℓy}, its positivity, the bound w(y) ≤ (32 y + 11) e^{-π y} for y > 0 (a crude form of (6.11)), and measurability on (0, ∞).

noncomputable def Zeta5Irrational.wS (y : ℝ) : ℝ

The series ∑_{ℓ ≥ 1} ℓ⁴ e^{-2πℓy}.

Equations

• Zeta5Irrational.wS y = ∑' (ℓ : ℕ), (↑ℓ + 1) ^ 4 * Real.exp (-(2 * Real.pi * (↑ℓ + 1) * y))

noncomputable def Zeta5Irrational.w (y : ℝ) : ℝ

The weight w(y) = (2π)⁴ y⁵ / 12 · ∑_{ℓ ≥ 1} ℓ⁴ e^{-2πℓy} of (2.10).

Equations

• Zeta5Irrational.w y = (2 * Real.pi) ^ 4 * y ^ 5 / 12 * Zeta5Irrational.wS y

theorem Zeta5Irrational.summable_w_term {y : ℝ} (hy : 0 < y) : Summable fun (ℓ : ℕ) => (↑ℓ + 1) ^ 4 * Real.exp (-(2 * Real.pi * (↑ℓ + 1) * y))

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

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

theorem Zeta5Irrational.one_div_one_sub_exp_neg_le {x : ℝ} (hx : 0 < x) : 1 / (1 - Real.exp (-x)) ≤ 1 + 1 / x

1 / (1 - e^{-x}) ≤ 1 + 1 / x for x > 0.

theorem Zeta5Irrational.wS_le {y : ℝ} (hy : 0 < y) : wS y ≤ 24 / (Real.pi * y) ^ 4 * (1 + 1 / (Real.pi * y)) * Real.exp (-(Real.pi * y))

The bound wS y ≤ 24 (1 + 1/(πy)) e^{-πy} / (πy)⁴.

theorem Zeta5Irrational.w_le {y : ℝ} (hy : 0 < y) : w y ≤ (32 * y + 11) * Real.exp (-(Real.pi * y))

The bound w(y) ≤ (32 y + 11) e^{-πy} for y > 0.

theorem Zeta5Irrational.aemeasurable_wS : AEMeasurable wS (MeasureTheory.volume.restrict (Set.Ioi 0))

wS is a.e.-measurable on (0, ∞), as the pointwise limit of continuous partial sums.

theorem Zeta5Irrational.aemeasurable_w : AEMeasurable w (MeasureTheory.volume.restrict (Set.Ioi 0))