Gauss Digamma Eq Digamma

Supporting definitions and lemmas for the Odlyzko-bound formalization.

noncomputable def NumberField.Odlyzko.gaussDigammaIntegrand (s : ℂ) (x : ℝ) : ℂ

A gauss digamma integrand used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.gaussDigammaIntegrand s x = (Complex.exp (-↑x) - Complex.exp (-s * ↑x)) / (1 - Complex.exp (-↑x))

theorem NumberField.Odlyzko.integral_cexp_neg_mul_Ioi {s : ℂ} (hs : 0 < s.re) : ∫ (x : ℝ) in Set.Ioi 0, Complex.exp (-s * ↑x) = 1 / s

theorem NumberField.Odlyzko.half_mul_le_one_sub_exp_neg {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : x / 2 ≤ 1 - Real.exp (-x)

theorem NumberField.Odlyzko.norm_gaussDigammaIntegrand_le_local (s : ℂ) {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) (hsx : ‖s - 1‖ * x ≤ 1) : ‖gaussDigammaIntegrand s x‖ ≤ 4 * ‖s - 1‖

theorem NumberField.Odlyzko.norm_gaussDigammaIntegrand_le_tail {s : ℂ} (_hs : 0 < s.re) {x : ℝ} (hx : 1 ≤ x) : ‖gaussDigammaIntegrand s x‖ ≤ (1 - Real.exp (-1))⁻¹ * (Real.exp (-x) + Real.exp (-s.re * x))

theorem NumberField.Odlyzko.gaussDigammaIntegrand_integrableOn_Ioi_one {s : ℂ} (hs : 0 < s.re) : MeasureTheory.IntegrableOn (gaussDigammaIntegrand s) (Set.Ioi 1) MeasureTheory.volume

noncomputable def NumberField.Odlyzko.gaussDigammaLocalRadius (s : ℂ) : ℝ

A gauss digamma local radius used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.gaussDigammaLocalRadius s = min 1 (1 / (1 + ‖s - 1‖))

theorem NumberField.Odlyzko.norm_mul_gaussDigammaLocalRadius_le_one (s : ℂ) : ‖s - 1‖ * gaussDigammaLocalRadius s ≤ 1

theorem NumberField.Odlyzko.gaussDigammaIntegrand_integrableOn_Ioc_zero_localRadius (s : ℂ) : MeasureTheory.IntegrableOn (gaussDigammaIntegrand s) (Set.Ioc 0 (gaussDigammaLocalRadius s)) MeasureTheory.volume

theorem NumberField.Odlyzko.gaussDigammaIntegrand_integrableOn_Ioi {s : ℂ} (hs : 0 < s.re) : MeasureTheory.IntegrableOn (gaussDigammaIntegrand s) (Set.Ioi 0) MeasureTheory.volume

noncomputable def NumberField.Odlyzko.gaussDigamma (s : ℂ) : ℂ

A gauss digamma used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.gaussDigamma s = -↑Real.eulerMascheroniConstant + ∫ (x : ℝ) in Set.Ioi 0, NumberField.Odlyzko.gaussDigammaIntegrand s x

noncomputable def NumberField.Odlyzko.gaussDigammaPartialIntegrand (s : ℂ) (n : ℕ) (x : ℝ) : ℂ

A gauss digamma partial integrand used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.gaussDigammaPartialIntegrand s n x = ∑ k ∈ Finset.range n, (Complex.exp (-(↑k + 1) * ↑x) - Complex.exp (-(s + ↑k) * ↑x))

noncomputable def NumberField.Odlyzko.gaussDigammaPartialSum (s : ℂ) (n : ℕ) : ℂ

A gauss digamma partial sum used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.gaussDigammaPartialSum s n = ∑ k ∈ Finset.range n, ((↑(k + 1))⁻¹ - (s + ↑k)⁻¹)

theorem NumberField.Odlyzko.gaussDigammaPartialIntegrand_eq (s : ℂ) (n : ℕ) {x : ℝ} (hx : x ≠ 0) : gaussDigammaPartialIntegrand s n x = (1 - Complex.exp (-↑n * ↑x)) * gaussDigammaIntegrand s x

theorem NumberField.Odlyzko.integral_gaussDigammaPartialIntegrand {s : ℂ} (hs : 0 < s.re) (n : ℕ) : ∫ (x : ℝ) in Set.Ioi 0, gaussDigammaPartialIntegrand s n x = gaussDigammaPartialSum s n

theorem NumberField.Odlyzko.tendsto_integral_gaussDigammaPartialIntegrand {s : ℂ} (hs : 0 < s.re) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ) in Set.Ioi 0, gaussDigammaPartialIntegrand s n x) Filter.atTop (nhds (∫ (x : ℝ) in Set.Ioi 0, gaussDigammaIntegrand s x))

theorem NumberField.Odlyzko.tendsto_gaussDigammaPartialSum {s : ℂ} (hs : 0 < s.re) : Filter.Tendsto (gaussDigammaPartialSum s) Filter.atTop (nhds (∫ (x : ℝ) in Set.Ioi 0, gaussDigammaIntegrand s x))

theorem NumberField.Odlyzko.logDeriv_natCast_cpow {n : ℕ} (hn : n ≠ 0) (s : ℂ) : logDeriv (fun (z : ℂ) => ↑n ^ z) s = Complex.log ↑n

theorem NumberField.Odlyzko.logDeriv_GammaSeq {s : ℂ} {n : ℕ} (hn : n ≠ 0) (hs : ∀ j ∈ Finset.range (n + 1), s + ↑j ≠ 0) : logDeriv (fun (z : ℂ) => z.GammaSeq n) s = Complex.log ↑n - ∑ j ∈ Finset.range (n + 1), (s + ↑j)⁻¹

theorem NumberField.Odlyzko.logDeriv_GammaSeq_succ_eq {s : ℂ} (hs : 0 < s.re) (n : ℕ) : logDeriv (fun (z : ℂ) => z.GammaSeq (n + 1)) s = gaussDigammaPartialSum s (n + 1) - ↑(Real.eulerMascheroniSeq' (n + 1)) - (s + ↑(n + 1))⁻¹

noncomputable def NumberField.Odlyzko.gaussDigammaSeriesTerm (k : ℕ) (s : ℂ) : ℂ

A gauss digamma series term used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.gaussDigammaSeriesTerm k s = (↑(k + 1))⁻¹ - (s + ↑k)⁻¹

theorem NumberField.Odlyzko.gaussDigammaSeriesTerm_eq_div {s : ℂ} (hs : 0 < s.re) (k : ℕ) : gaussDigammaSeriesTerm k s = (s - 1) / (↑(k + 1) * (s + ↑k))

theorem NumberField.Odlyzko.norm_gaussDigammaSeriesTerm_le {M : ℝ} {s : ℂ} (hs : 0 < s.re) (hsM : ‖s - 1‖ ≤ M) {k : ℕ} (hk : 1 ≤ k) : ‖gaussDigammaSeriesTerm k s‖ ≤ M / ↑k ^ 2

theorem NumberField.Odlyzko.tendstoUniformlyOn_gaussDigammaPartialSum (M : ℝ) : TendstoUniformlyOn (fun (n : ℕ) (s : ℂ) => gaussDigammaPartialSum s n) (fun (s : ℂ) => ∑' (k : ℕ), gaussDigammaSeriesTerm k s) Filter.atTop {s : ℂ | 0 < s.re ∧ ‖s - 1‖ ≤ M}

theorem NumberField.Odlyzko.tsum_gaussDigammaSeriesTerm_eq_integral {s : ℂ} (hs : 0 < s.re) : ∑' (k : ℕ), gaussDigammaSeriesTerm k s = ∫ (x : ℝ) in Set.Ioi 0, gaussDigammaIntegrand s x

theorem NumberField.Odlyzko.tendstoLocallyUniformlyOn_gaussDigammaPartialSum : TendstoLocallyUniformlyOn (fun (n : ℕ) (s : ℂ) => gaussDigammaPartialSum s n) (fun (s : ℂ) => ∫ (x : ℝ) in Set.Ioi 0, gaussDigammaIntegrand s x) Filter.atTop {s : ℂ | 0 < s.re}

theorem NumberField.Odlyzko.norm_inv_add_natCast_le {s : ℂ} (hs : 0 < s.re) {n : ℕ} (hn : 1 ≤ n) : ‖(s + ↑n)⁻¹‖ ≤ 1 / ↑n

theorem NumberField.Odlyzko.tendstoUniformlyOn_inv_add_natCast_succ : TendstoUniformlyOn (fun (n : ℕ) (s : ℂ) => (s + ↑(n + 1))⁻¹) (fun (x : ℂ) => 0) Filter.atTop {s : ℂ | 0 < s.re}

theorem NumberField.Odlyzko.tendstoLocallyUniformlyOn_logDeriv_GammaSeq_succ : TendstoLocallyUniformlyOn (fun (n : ℕ) (s : ℂ) => logDeriv (fun (z : ℂ) => z.GammaSeq (n + 1)) s) gaussDigamma Filter.atTop {s : ℂ | 0 < s.re}

noncomputable def NumberField.Odlyzko.gammaSeqApproxIntegrand (n : ℕ) (s : ℂ) (x : ℝ) : ℂ

A gamma seq approx integrand used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.gammaSeqApproxIntegrand n s x = (Set.Ioc 0 ↑n).indicator (fun (x : ℝ) => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) x

noncomputable def NumberField.Odlyzko.gammaIntegralIntegrand (s : ℂ) (x : ℝ) : ℂ

A gamma integral integrand used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.gammaIntegralIntegrand s x = (Set.Ioi 0).indicator (fun (x : ℝ) => ↑(Real.exp (-x)) * ↑x ^ (s - 1)) x

noncomputable def NumberField.Odlyzko.gammaVerticalMajorant (a b x : ℝ) : ℝ

A gamma vertical majorant used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.gammaVerticalMajorant a b x = (Set.Ioi 0).indicator (fun (x : ℝ) => Real.exp (-x) * (x ^ (a - 1) + x ^ (b - 1))) x

theorem NumberField.Odlyzko.integral_gammaSeqApproxIntegrand {s : ℂ} (hs : 0 < s.re) {n : ℕ} (hn : n ≠ 0) : ∫ (x : ℝ), gammaSeqApproxIntegrand n s x = s.GammaSeq n

theorem NumberField.Odlyzko.integral_gammaIntegralIntegrand {s : ℂ} (hs : 0 < s.re) : ∫ (x : ℝ), gammaIntegralIntegrand s x = Complex.Gamma s

theorem NumberField.Odlyzko.rpow_re_sub_one_le_endpoint_sum {a b x : ℝ} {s : ℂ} (hx : 0 < x) (ha : a ≤ s.re) (hb : s.re ≤ b) : x ^ (s.re - 1) ≤ x ^ (a - 1) + x ^ (b - 1)

noncomputable def NumberField.Odlyzko.gammaSeqScalarKernel (n : ℕ) (x : ℝ) : ℝ

A gamma seq scalar kernel used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.gammaSeqScalarKernel n x = (Set.Ioc 0 ↑n).indicator (fun (x : ℝ) => (1 - x / ↑n) ^ n) x

noncomputable def NumberField.Odlyzko.gammaScalarKernel (x : ℝ) : ℝ

A gamma scalar kernel used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.gammaScalarKernel x = (Set.Ioi 0).indicator (fun (x : ℝ) => Real.exp (-x)) x

noncomputable def NumberField.Odlyzko.gammaSeqIntegralError (a b : ℝ) (n : ℕ) (x : ℝ) : ℝ

A gamma seq integral error used in the Odlyzko-bound argument.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.Odlyzko.integrable_gammaVerticalMajorant {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : MeasureTheory.Integrable (gammaVerticalMajorant a b) MeasureTheory.volume

theorem NumberField.Odlyzko.gammaSeqScalarKernel_le (n : ℕ) (x : ℝ) : gammaSeqScalarKernel n x ≤ gammaScalarKernel x

theorem NumberField.Odlyzko.tendsto_gammaSeqScalarKernel (x : ℝ) : Filter.Tendsto (fun (n : ℕ) => gammaSeqScalarKernel n x) Filter.atTop (nhds (gammaScalarKernel x))

theorem NumberField.Odlyzko.tendsto_gammaSeqIntegralError (a b x : ℝ) : Filter.Tendsto (fun (n : ℕ) => gammaSeqIntegralError a b n x) Filter.atTop (nhds 0)

theorem NumberField.Odlyzko.gammaSeqIntegralError_le_majorant (a b : ℝ) (n : ℕ) (x : ℝ) : gammaSeqIntegralError a b n x ≤ gammaVerticalMajorant a b x

theorem NumberField.Odlyzko.gammaSeqIntegralError_nonneg (a b : ℝ) (n : ℕ) (x : ℝ) : 0 ≤ gammaSeqIntegralError a b n x

theorem NumberField.Odlyzko.aestronglyMeasurable_gammaSeqIntegralError (a b : ℝ) (n : ℕ) : MeasureTheory.AEStronglyMeasurable (gammaSeqIntegralError a b n) MeasureTheory.volume

theorem NumberField.Odlyzko.integrable_gammaSeqIntegralError {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (n : ℕ) : MeasureTheory.Integrable (gammaSeqIntegralError a b n) MeasureTheory.volume

theorem NumberField.Odlyzko.tendsto_integral_gammaSeqIntegralError {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ), gammaSeqIntegralError a b n x) Filter.atTop (nhds 0)

theorem NumberField.Odlyzko.integrable_gammaSeqApproxIntegrand {s : ℂ} (hs : 0 < s.re) (n : ℕ) : MeasureTheory.Integrable (gammaSeqApproxIntegrand n s) MeasureTheory.volume

theorem NumberField.Odlyzko.integrable_gammaIntegralIntegrand {s : ℂ} (hs : 0 < s.re) : MeasureTheory.Integrable (gammaIntegralIntegrand s) MeasureTheory.volume

theorem NumberField.Odlyzko.norm_gammaSeqApproxIntegrand_sub_le_error {a b : ℝ} {s : ℂ} (ha : a ≤ s.re) (hb : s.re ≤ b) (n : ℕ) (x : ℝ) : ‖gammaSeqApproxIntegrand n s x - gammaIntegralIntegrand s x‖ ≤ gammaSeqIntegralError a b n x

theorem NumberField.Odlyzko.norm_integral_gammaSeqApproxIntegrand_sub_le {a b : ℝ} (ha0 : 0 < a) (hb0 : 0 < b) {s : ℂ} (ha : a ≤ s.re) (hb : s.re ≤ b) (n : ℕ) : ‖(∫ (x : ℝ), gammaSeqApproxIntegrand n s x) - ∫ (x : ℝ), gammaIntegralIntegrand s x‖ ≤ ∫ (x : ℝ), gammaSeqIntegralError a b n x

theorem NumberField.Odlyzko.tendstoUniformlyOn_integral_gammaSeqApproxIntegrand {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : TendstoUniformlyOn (fun (n : ℕ) (s : ℂ) => ∫ (x : ℝ), gammaSeqApproxIntegrand n s x) (fun (s : ℂ) => ∫ (x : ℝ), gammaIntegralIntegrand s x) Filter.atTop {s : ℂ | a ≤ s.re ∧ s.re ≤ b}

theorem NumberField.Odlyzko.tendstoUniformlyOn_GammaSeq {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : TendstoUniformlyOn (fun (n : ℕ) (s : ℂ) => s.GammaSeq n) Complex.Gamma Filter.atTop {s : ℂ | a ≤ s.re ∧ s.re ≤ b}

theorem NumberField.Odlyzko.tendstoLocallyUniformlyOn_GammaSeq : TendstoLocallyUniformlyOn (fun (n : ℕ) (s : ℂ) => s.GammaSeq n) Complex.Gamma Filter.atTop {s : ℂ | 0 < s.re}

theorem NumberField.Odlyzko.tendstoLocallyUniformlyOn_GammaSeq_succ : TendstoLocallyUniformlyOn (fun (n : ℕ) (s : ℂ) => s.GammaSeq (n + 1)) Complex.Gamma Filter.atTop {s : ℂ | 0 < s.re}

theorem NumberField.Odlyzko.differentiableOn_GammaSeq_succ (n : ℕ) : DifferentiableOn ℂ (fun (s : ℂ) => s.GammaSeq (n + 1)) {s : ℂ | 0 < s.re}

theorem NumberField.Odlyzko.gaussDigamma_eq_digamma {s : ℂ} (hs : 0 < s.re) : gaussDigamma s = s.digamma