LeanPool.Zeta3Irrational.Integral

theorem LeanPool.Zeta3Irrational.Nat_Ico_succ_right (a b : ℕ) : Finset.Ico a (b + 1) = Finset.Icc a b

theorem LeanPool.Zeta3Irrational.Nat_Ico_succ_succ (a b : ℕ) : Finset.Ico (a + 1) (b + 1) = Finset.Ioc a b

@[reducible, inline]

noncomputable abbrev LeanPool.Zeta3Irrational.J (r s : ℕ) : ℝ

The two-variable Apéry integral with monomial weights.

Equations

• LeanPool.Zeta3Irrational.J r s = ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * x.1 ^ r * x.2 ^ s

@[reducible, inline]

noncomputable abbrev LeanPool.Zeta3Irrational.JENN (r s : ℕ) : ENNReal

The extended nonnegative version of J.

Equations

• LeanPool.Zeta3Irrational.JENN r s = ∫⁻ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ENNReal.ofReal (-Real.log (x.1 * x.2) / (1 - x.1 * x.2) * x.1 ^ r * x.2 ^ s)

theorem LeanPool.Zeta3Irrational.log_rpow_integral_aux (n a : ℝ) (ha : 0 < a ∧ a ≤ 1) : ∫ (x : ℝ) in Set.Ioc a 1, |-Real.log x * x ^ n| = ∫ (x : ℝ) in Set.Ioc a 1, -Real.log x * x ^ n

theorem LeanPool.Zeta3Irrational.log_rpow_integral' (n : ℝ) (hn : n > -1) (a : ℝ) (ha : 0 < a ∧ a ≤ 1) : ∫ (x : ℝ) in Set.Ioc a 1, -Real.log x * x ^ n = 1 / (n + 1) ^ 2 - (a ^ (n + 1) / (n + 1) ^ 2 - a ^ (n + 1) * Real.log a / (n + 1))

theorem LeanPool.Zeta3Irrational.log_rpow_integrable (n : ℝ) (hn : n > -1) : IntervalIntegrable (fun (x : ℝ) => -Real.log x * x ^ n) MeasureTheory.volume 0 1

theorem LeanPool.Zeta3Irrational.log_rpow_integral (n : ℝ) (hn : n > -1) : ∫ (x : ℝ) in 0..1, -Real.log x * x ^ n = 1 / (n + 1) ^ 2

theorem LeanPool.Zeta3Irrational.ENN_log_rpow_integral (n : ℝ) (hn : n > -1) : ∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (-Real.log x * x ^ n) = ENNReal.ofReal (1 / (n + 1) ^ 2)

theorem LeanPool.Zeta3Irrational.ENN_log_pow_integral (n : ℕ) : ∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (-Real.log x * x ^ n) = ENNReal.ofReal (1 / (↑n + 1) ^ 2)

theorem LeanPool.Zeta3Irrational.ENN_pow_integral (n : ℕ) : ∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (x ^ n) = ENNReal.ofReal (1 / (↑n + 1))

theorem LeanPool.Zeta3Irrational.AEMeasurable_aux {r s : ℕ} : AEMeasurable (fun (x : ℝ × ℝ × ℝ) => 1 / (1 - (1 - x.2.1 * x.2.2) * x.1) * x.2.1 ^ r * x.2.2 ^ s) MeasureTheory.volume

theorem LeanPool.Zeta3Irrational.integral1 {a : ℝ} (ha : 0 < a) (ha1 : a < 1) : ∫ (z : ℝ) in 0..1, 1 / (1 - (1 - a) * z) = -Real.log a / (1 - a)

theorem LeanPool.Zeta3Irrational.sub_mul_mul_ne_zero (y : ℝ) (x : ℝ × ℝ) (hy : y ∈ Set.Icc 0 1) (h1 : 0 < 1 - (1 - x.1 * x.2)) : 1 - (1 - x.1 * x.2) * y ≠ 0

theorem LeanPool.Zeta3Irrational.integrableOn_aux (x : ℝ × ℝ) (h1 : 0 < 1 - (1 - x.1 * x.2)) (h2 : 1 - (1 - x.1 * x.2) < 1) : MeasureTheory.IntegrableOn (fun (t : ℝ) => 1 / (1 - (1 - x.1 * x.2) * t)) (Set.Ioo 0 1) MeasureTheory.volume

theorem LeanPool.Zeta3Irrational.JENN_eq_triple_aux' (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) : ∫⁻ (w : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (1 / (1 - (1 - x.1 * x.2) * w)) = ENNReal.ofReal (-Real.log (1 - (1 - x.1 * x.2)) / (1 - x.1 * x.2))

theorem LeanPool.Zeta3Irrational.JENN_eq_triple_aux {r s : ℕ} (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) : ∫⁻ (w : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (1 / (1 - (1 - x.1 * x.2) * w) * x.1 ^ r * x.2 ^ s) = ENNReal.ofReal (-Real.log (x.1 * x.2) / (1 - x.1 * x.2) * x.1 ^ r * x.2 ^ s)

theorem LeanPool.Zeta3Irrational.JENN_eq_triple (r s : ℕ) : JENN r s = ∫⁻ (x : ℝ × ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ENNReal.ofReal (1 / (1 - (1 - x.2.1 * x.2.2) * x.1) * x.2.1 ^ r * x.2.2 ^ s)

theorem LeanPool.Zeta3Irrational.AEMeasurable_aux' {k r s : ℕ} : AEMeasurable (fun (x : ℝ × ℝ) => ENNReal.ofReal (-Real.log (x.1 * x.2) * x.1 ^ (k + r) * x.2 ^ (k + s))) (MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1))

theorem LeanPool.Zeta3Irrational.aux_lintegral1 (k r s : ℕ) (x : ℝ) (hx : 0 < x ∧ x < 1) : ∫⁻ (a : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (-(Real.log x * x ^ (k + r) * a ^ (k + s))) = ENNReal.ofReal (-Real.log x * x ^ (k + r) / (↑k + ↑s + 1))

theorem LeanPool.Zeta3Irrational.aux_lintegral2 (k r s : ℕ) (x : ℝ) (hx : 0 < x ∧ x < 1) : ∫⁻ (a : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (-(Real.log a * x ^ (k + r) * a ^ (k + s))) = ENNReal.ofReal (x ^ (k + r) / (↑k + ↑s + 1) ^ 2)

theorem LeanPool.Zeta3Irrational.aux_lintegral3 (k r s : ℕ) : ∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (-Real.log x * x ^ (k + r) / (↑k + ↑s + 1)) = ENNReal.ofReal (1 / ((↑k + ↑r + 1) ^ 2 * (↑k + ↑s + 1)))

theorem LeanPool.Zeta3Irrational.aux_lintegral4 (k r s : ℕ) : ∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (x ^ (k + r) / (↑k + ↑s + 1) ^ 2) = ENNReal.ofReal (1 / ((↑k + ↑r + 1) * (↑k + ↑s + 1) ^ 2))

theorem LeanPool.Zeta3Irrational.J_ENN_rs_eq_tsum_aux_intergal (r s k : ℕ) : ∫⁻ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ENNReal.ofReal (-Real.log (x.1 * x.2) * x.1 ^ (k + r) * x.2 ^ (k + s)) = ENNReal.ofReal (1 / ((↑k + ↑r + 1) ^ 2 * (↑k + ↑s + 1)) + 1 / ((↑k + ↑r + 1) * (↑k + ↑s + 1) ^ 2))

theorem LeanPool.Zeta3Irrational.J_ENN_rs_eq_tsum (r s : ℕ) : JENN r s = ∑' (k : ℕ), ENNReal.ofReal (1 / ((↑k + ↑r + 1) ^ 2 * (↑k + ↑s + 1)) + 1 / ((↑k + ↑r + 1) * (↑k + ↑s + 1) ^ 2))

theorem LeanPool.Zeta3Irrational.J_ENN_rr (r : ℕ) : JENN r r = ENNReal.ofReal (2 * ∑' (n : ℕ), 1 / (↑n + 1) ^ 3 - 2 * ∑ m ∈ Finset.Icc 1 r, 1 / ↑m ^ 3)

theorem LeanPool.Zeta3Irrational.fun_of_J_nonneg (r s : ℕ) (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) : 0 ≤ -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * x.1 ^ r * x.2 ^ s

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

theorem LeanPool.Zeta3Irrational.J_rr (r : ℕ) : J r r = 2 * ∑' (n : ℕ), 1 / (↑n + 1) ^ 3 - 2 * ∑ m ∈ Finset.Icc 1 r, 1 / ↑m ^ 3

theorem LeanPool.Zeta3Irrational.zeta3 : J 0 0 = 2 * ∑' (n : ℕ), 1 / (↑n + 1) ^ 3

theorem LeanPool.Zeta3Irrational.positivity_aux (r s : ℕ) (h : r > s) (i : ℕ) : 0 ≤ 1 / (↑r - ↑s) * (1 / (↑i + ↑s + 1) ^ 2 - 1 / (↑i + ↑r + 1) ^ 2)

theorem LeanPool.Zeta3Irrational.summable_aux (r : ℕ) : Summable fun (b : ℕ) => 1 / (↑b + ↑r + 1) ^ 2

theorem LeanPool.Zeta3Irrational.J_ENN_rs (r s : ℕ) (h : r > s) : JENN r s = ENNReal.ofReal ((∑ k ∈ Finset.Ioc s r, 1 / ↑k ^ 2) / (↑r - ↑s))

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

theorem LeanPool.Zeta3Irrational.J_rs' (r s : ℕ) (h : r > s) : J r s = (∑ k ∈ Finset.Ioc s r, 1 / ↑k ^ 2) / (↑r - ↑s)

theorem LeanPool.Zeta3Irrational.J_ENN_rs_symm (r s : ℕ) : JENN r s = JENN s r

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

theorem LeanPool.Zeta3Irrational.J_eq_toReal_J_ENN (r s : ℕ) : J r s = (JENN r s).toReal

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

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