LeanPool.Zeta3Irrational.LinearForm

theorem LeanPool.Zeta3Irrational.d_cube_ne_zero {r : ℕ} : ↑(d (Finset.Icc 1 r)) ^ 3 ≠ 0

theorem LeanPool.Zeta3Irrational.J_rr_linear (r : ℕ) : ∃ (a : ℤ), J r r = 2 * ∑' (n : ℕ), 1 / (↑n + 1) ^ 3 - ↑a / ↑(d (Finset.Icc 1 r)) ^ 3

theorem LeanPool.Zeta3Irrational.Icc_diff_Icc {r s : ℕ} : r > s → ¬s = 0 → Finset.Icc 1 r \ Finset.Icc 1 s = Finset.Icc (s + 1) r

theorem LeanPool.Zeta3Irrational.one_div_sum_eq {r s : ℕ} (h : r > s) : ∑ m ∈ Finset.Icc 1 r, 1 / ↑m ^ 2 - ∑ m ∈ Finset.Icc 1 s, 1 / ↑m ^ 2 = ∑ m ∈ Finset.Icc 1 (r - s), 1 / (↑s + ↑m) ^ 2

theorem LeanPool.Zeta3Irrational.J_rs_linear {r s : ℕ} (h : r > s) : ∃ (a : ℤ), J r s = ↑a / ↑(d (Finset.Icc 1 r)) ^ 3

theorem LeanPool.Zeta3Irrational.integrableOn_weighted_J (r s : ℕ) (p q : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ × ℝ) => -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * p * x.1 ^ r * q * x.2 ^ s) (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) MeasureTheory.volume

Constant monomial weights preserve integrability of the Apéry integrand.

theorem LeanPool.Zeta3Irrational.multi_integral_sum_comm {n : ℕ} (c : ℕ → ℤ) : ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ∑ x_1 ∈ Finset.range (n + 1), ∑ x_2 ∈ Finset.range (n + 1), -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * ↑(c x_1) * x.1 ^ x_1 * ↑(c x_2) * x.2 ^ x_2 = ∑ x_1 ∈ Finset.range (n + 1), ∑ x_2 ∈ Finset.range (n + 1), ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * ↑(c x_1) * x.1 ^ x_1 * ↑(c x_2) * x.2 ^ x_2

theorem LeanPool.Zeta3Irrational.multi_integral_mul_const (c d : ℕ) (p q : ℝ) : ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * p * x.1 ^ c * q * x.2 ^ d = p * q * J c d

noncomputable def LeanPool.Zeta3Irrational.p (r s : ℕ) : ℤ

The integer coefficient of the rational part of J r s.

Equations

• LeanPool.Zeta3Irrational.p r s = if h : r > s then ⋯.choose else if h : r < s then ⋯.choose else -⋯.choose

noncomputable def LeanPool.Zeta3Irrational.q (r s : ℕ) : ℤ

The integer coefficient of the zeta part of J r s.

Equations

• LeanPool.Zeta3Irrational.q r s = if r > s then 0 else if r < s then 0 else 2

theorem LeanPool.Zeta3Irrational.J_symm (r s : ℕ) : J r s = J s r

theorem LeanPool.Zeta3Irrational.linear_int_aux : ∃ (a : ℕ → ℕ → ℤ) (b : ℕ → ℕ → ℤ), ∀ (r s : ℕ), J r s = ↑(b r s) * ∑' (n : ℕ), 1 / (↑n + 1) ^ 3 + ↑(a r s) / ↑(d (Finset.Icc 1 (r.max s))) ^ 3