Documentation

LeanPool.Zeta3Irrational.Basic

LeanPool.Zeta3Irrational.Basic #

source
@[reducible, inline]
noncomputable abbrev LeanPool.Zeta3Irrational.JJ (n : ℕ) :
ℝ

The Apéry integral after inserting two shifted Legendre polynomials.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible, inline]
    noncomputable abbrev LeanPool.Zeta3Irrational.JJ' (n : ℕ) :
    ℝ

    The transformed three-variable form of the Apéry integral.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev LeanPool.Zeta3Irrational.JJENN (n : ℕ) :
      ENNReal

      The extended nonnegative integral associated to JJ'.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev LeanPool.Zeta3Irrational.fun1 (n : ℕ) :
        ℝ

        The denominator-cleared Apéry linear form.

        Equations
        Instances For
          source
          theorem LeanPool.Zeta3Irrational.linear_int (n : ℕ) :
          ∃ (a : ℕ → ℤ) (b : ℕ → ℤ), fun1 n = ↑(a n) + ↑(b n) * ↑↑(d (Finset.Icc 1 n)) ^ 3 * ∑' (n : ℕ), 1 / (↑n + 1) ^ 3
          source
          theorem LeanPool.Zeta3Irrational.pos_aux (x : ℝ × ℝ × ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ (0 < x.2.1 ∧ x.2.1 < 1) ∧ 0 < x.2.2 ∧ x.2.2 < 1) :
          0 < 1 - (1 - x.2.1 * x.2.2) * x.1
          source
          theorem LeanPool.Zeta3Irrational.JJENN_upper (n : ℕ) :
          JJENN n ≤ ENNReal.ofReal (2 * (1 / 30) ^ n * ∑' (n : ℕ), 1 / (↑n + 1) ^ 3)
          source
          theorem LeanPool.Zeta3Irrational.integrableOn_JJ' (n : ℕ) :
          MeasureTheory.Integrable (fun (x : ℝ × ℝ × ℝ) => (x.2.1 * (1 - x.2.1) * x.2.2 * (1 - x.2.2) * x.1 * (1 - x.1) / (1 - (1 - x.2.1 * x.2.2) * x.1)) ^ n / (1 - (1 - x.2.1 * x.2.2) * x.1)) (MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1))
          source
          theorem LeanPool.Zeta3Irrational.shiftedLegendre_bound (n : ℕ) (x : ℝ) (hx : 0 < x ∧ x < 1) :
          |Polynomial.eval x (Polynomial.shiftedLegendre n)| ≤ ∑ x_1 ∈ Finset.range (n + 1), ↑(n.choose x_1) * ↑((n + x_1).choose n)
          source
          theorem LeanPool.Zeta3Irrational.Measurable_one_div_aux :
          Measurable fun (x : ℝ × ℝ × ℝ) => ENNReal.ofReal (1 / (1 - (1 - x.2.1 * x.2.2) * x.1))
          source
          theorem LeanPool.Zeta3Irrational.integrableOn_JJ1 (n : ℕ) :
          MeasureTheory.Integrable (Function.uncurry fun (z : ℝ) (x : ℝ × ℝ) => Polynomial.eval x.1 (Polynomial.shiftedLegendre n) * Polynomial.eval x.2 (Polynomial.shiftedLegendre n) * (1 / (1 - (1 - x.1 * x.2) * z))) ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1)))
          source
          theorem LeanPool.Zeta3Irrational.integrableOn_JJ2 (n : ℕ) :
          MeasureTheory.Integrable (Function.uncurry fun (z : ℝ) (x : ℝ × ℝ) => Polynomial.eval x.1 (Polynomial.shiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1)) ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1)))
          source
          theorem LeanPool.Zeta3Irrational.integrableOn_JJ3 (n : ℕ) :
          MeasureTheory.Integrable (Function.uncurry fun (z : ℝ) (x : ℝ × ℝ) => Polynomial.eval x.1 (Polynomial.shiftedLegendre n) * (1 - z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z)) ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1)))
          source
          theorem LeanPool.Zeta3Irrational.eq1_integrableOn_aux1 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) :
          MeasureTheory.Integrable (fun (x : ℝ × ℝ) => Polynomial.eval x.1 (Polynomial.shiftedLegendre n) * Polynomial.eval x.2 (Polynomial.shiftedLegendre n) * (1 / (1 - (1 - x.1 * x.2) * z))) ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 1)))
          source
          theorem LeanPool.Zeta3Irrational.eq1_integrableOn_aux2 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) :
          MeasureTheory.Integrable (fun (x : ℝ × ℝ) => Polynomial.eval x.1 (Polynomial.shiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1)) ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 1)))
          source
          theorem LeanPool.Zeta3Irrational.double_integral_eq1 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) :
          ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, Polynomial.eval x.1 (Polynomial.shiftedLegendre n) * Polynomial.eval x.2 (Polynomial.shiftedLegendre n) * (1 / (1 - (1 - x.1 * x.2) * z)) = ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, Polynomial.eval x.1 (Polynomial.shiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1)
          source
          theorem LeanPool.Zeta3Irrational.ineq_aux (x : ℝ × ℝ) (z : ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ 0 < x.2 ∧ x.2 < 1) (hz : 0 ≤ z ∧ z ≤ 1) :
          0 ≤ (1 - z) / (1 - (1 - x.1 * x.2) * z) ∧ (1 - z) / (1 - (1 - x.1 * x.2) * z) ≤ 1
          source
          theorem LeanPool.Zeta3Irrational.ineq_aux1 (x : ℝ × ℝ) (z : ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ 0 < x.2 ∧ x.2 < 1) (hz : 0 ≤ z ∧ z ≤ 1) :
          1 - (1 - x.1 * x.2) * z ≠ 0
          source
          theorem LeanPool.Zeta3Irrational.fun_eq_aux (x : ℝ × ℝ) (y : ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ 0 < x.2 ∧ x.2 < 1) (hy : 0 ≤ y ∧ y ≤ 1) :
          deriv (fun (z : ℝ) => (1 - z) / (1 - (1 - x.1 * x.2) * z)) y = (fun (z : ℝ) => -x.1 * x.2 / (1 - (1 - x.1 * x.2) * z) ^ 2) y
          source
          theorem LeanPool.Zeta3Irrational.double_integral_eq2 (n : ℕ) (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) :
          ∫ (z : ℝ) in Set.Ioo 0 1, Polynomial.eval x.1 (Polynomial.shiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1) = ∫ (z : ℝ) in Set.Ioo 0 1, Polynomial.eval x.1 (Polynomial.shiftedLegendre n) * (1 - z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z)
          source
          theorem LeanPool.Zeta3Irrational.eq3_integrableOn_aux (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) :
          MeasureTheory.Integrable (fun (x : ℝ × ℝ) => Polynomial.eval x.1 (Polynomial.shiftedLegendre n) * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z)) ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 1)))
          source
          theorem LeanPool.Zeta3Irrational.double_integral_eq3 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) :
          ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, (x.1 * x.2 * z * (1 - x.1) * (1 - x.2)) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1) = ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, Polynomial.eval x.1 (Polynomial.shiftedLegendre n) * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z)
          source
          theorem LeanPool.Zeta3Irrational.JJ_eq_form (n : ℕ) :
          JJ n = JJ' n
          source
          theorem LeanPool.Zeta3Irrational.JJ_pos (n : ℕ) :
          0 < JJ n
          source
          theorem LeanPool.Zeta3Irrational.Summable_of_zeta_two' :
          Summable fun (n : ℕ) => 1 / (↑n + 1) ^ 2
          source
          theorem LeanPool.Zeta3Irrational.zeta3_pos :
          0 < ∑' (n : ℕ), 1 / (↑n + 1) ^ 3
          source
          theorem LeanPool.Zeta3Irrational.JJ_upper (n : ℕ) :
          JJ n ≤ 2 * (1 / 30) ^ n * ∑' (n : ℕ), 1 / (↑n + 1) ^ 3
          source
          theorem LeanPool.Zeta3Irrational.zeta3_le_zeta2 :
          ∑' (n : ℕ), 1 / (↑n + 1) ^ 3 < ∑' (n : ℕ), 1 / (↑n + 1) ^ 2
          source
          theorem LeanPool.Zeta3Irrational.eventually_d_pow_three_le_exp :
          ∀ᶠ (n : ℕ) in Filter.atTop, ↑(d (Finset.Icc 1 n)) ^ 3 ≤ Real.exp (339 / 100) ^ n
          source
          theorem LeanPool.Zeta3Irrational.fun1_tendsto_zero :
          Filter.Tendsto (fun (n : ℕ) => ENNReal.ofReal (fun1 n)) Filter.atTop (nhds 0)
          source
          theorem LeanPool.Zeta3Irrational.zeta3_irrational :
          ¬∃ (r : ℚ), ↑r = riemannZeta 3