@[reducible, inline]

abbrev ℙ : Type

Equations

• ℙ = Nat.Primes

theorem p_s_abs_1 (p : ℙ) (s : ℂ) (hs : 1 < s.re) : ‖↑↑p ^ (-s)‖ < 1

theorem zetaEulerprod (s : ℂ) (hs : 1 < s.re) : (Multipliable fun (p : ℙ) => (1 - ↑↑p ^ (-s))⁻¹) ∧ riemannZeta s = ∏' (p : ℙ), (1 - ↑↑p ^ (-s))⁻¹

theorem abs_of_tprod {P : Type u_1} (w : P → ℂ) (hw : Multipliable w) : ‖∏' (p : P), w p‖ = ∏' (p : P), ‖w p‖

theorem abs_P_prod (s : ℂ) (hs : 1 < s.re) : ‖∏' (p : ℙ), (1 - ↑↑p ^ (-s))⁻¹‖ = ∏' (p : ℙ), ‖(1 - ↑↑p ^ (-s))⁻¹‖

theorem abs_zeta_prod (s : ℂ) (hs : 1 < s.re) : ‖riemannZeta s‖ = ∏' (p : ℙ), ‖(1 - ↑↑p ^ (-s))⁻¹‖

theorem abs_of_inv (z : ℂ) (hz : z ≠ 0) : ‖z⁻¹‖ = ‖z‖⁻¹

theorem one_minus_p_s_neq_0 (p : ℙ) (s : ℂ) (hs : 1 < s.re) : 1 - ↑↑p ^ (-s) ≠ 0

theorem abs_zeta_prod_prime (s : ℂ) (hs : 1 < s.re) : ‖riemannZeta s‖ = ∏' (p : ℙ), ‖1 - ↑↑p ^ (-s)‖⁻¹

theorem Re2s (s : ℂ) : (2 * s).re = 2 * s.re

theorem Re2sge1 (s : ℂ) (hs : 1 < s.re) : 1 < (2 * s).re

theorem zeta_ratio_prod (s : ℂ) (hs : 1 < s.re) : riemannZeta (2 * s) / riemannZeta s = (∏' (p : ℙ), (1 - ↑↑p ^ (-(2 * s)))⁻¹) / ∏' (p : ℙ), (1 - ↑↑p ^ (-s))⁻¹

theorem tprod_commutes_with_inclusion_infinite {α : Type u_1} (f : α → ℂˣ) (h : Multipliable f) : (fun (z : ℂˣ) => ↑z) (tprod f) = ∏' (i : α), (fun (z : ℂˣ) => ↑z) (f i)

theorem inclusion_commutes_with_division (a b : ℂˣ) : (fun (z : ℂˣ) => ↑z) (a / b) = (fun (z : ℂˣ) => ↑z) a / (fun (z : ℂˣ) => ↑z) b

theorem lift_multipliable_of_nonzero {P : Type u_1} (a : P → ℂ) (ha : Multipliable a) (h_a_nonzero : ∀ (p : P), a p ≠ 0) (hA_nonzero' : ∀ (A : ℂ), HasProd a A → A ≠ 0) : Multipliable fun (p : P) => Units.mk0 (a p) ⋯

theorem prod_of_ratios_simplified {P : Type u_1} (a b : P → ℂ) (ha : Multipliable a) (hb : Multipliable b) (h_a_nonzero : ∀ (p : P), a p ≠ 0) (h_b_nonzero : ∀ (p : P), b p ≠ 0) (hA_nonzero' : ∀ (A : ℂ), HasProd a A → A ≠ 0) (hB_nonzero' : ∀ (A : ℂ), HasProd b A → A ≠ 0) : (∏' (p : P), a p) / ∏' (p : P), b p = ∏' (p : P), a p / b p

theorem prod_of_ratios {P : Type u_1} (a b : P → ℂ) (ha : Multipliable a) (hb : Multipliable b) (h_b_nonzero : ∀ (p : P), b p ≠ 0) (hA_nonzero' : ∀ (A : ℂ), HasProd a A → A ≠ 0) (hB_nonzero' : ∀ (B : ℂ), HasProd b B → B ≠ 0) : (∏' (p : P), a p) / ∏' (p : P), b p = ∏' (p : P), a p / b p

theorem simplify_prod_ratio (s : ℂ) (hs : 1 < s.re) : (∏' (p : ℙ), (1 - ↑↑p ^ (-(2 * s)))⁻¹) / ∏' (p : ℙ), (1 - ↑↑p ^ (-s))⁻¹ = ∏' (p : ℙ), (1 - ↑↑p ^ (-(2 * s)))⁻¹ / (1 - ↑↑p ^ (-s))⁻¹

theorem zeta_ratios (s : ℂ) (hs : 1 < s.re) : riemannZeta (2 * s) / riemannZeta s = ∏' (p : ℙ), (1 - ↑↑p ^ (-(2 * s)))⁻¹ / (1 - ↑↑p ^ (-s))⁻¹

theorem diff_of_squares (z : ℂ) : 1 - z ^ 2 = (1 - z) * (1 + z)

theorem one_sub_ne_zero_of_abs_lt_one (z : ℂ) (hz : ‖z‖ < 1) : 1 - z ≠ 0

theorem one_add_ne_zero_of_abs_lt_one (z : ℂ) (hz : ‖z‖ < 1) : 1 + z ≠ 0

theorem inv_mul_div_cancel_right_of_ne_zero (a b : ℂ) (ha : a ≠ 0) : (a * b)⁻¹ / a⁻¹ = b⁻¹

theorem ratio_invs (z : ℂ) (hz : ‖z‖ < 1) : (1 - z ^ 2)⁻¹ / (1 - z)⁻¹ = (1 + z)⁻¹

theorem complex_cpow_neg_two_mul (z w : ℂ) (hz : z ≠ 0) : z ^ (-(2 * w)) = (z ^ (-w)) ^ 2

theorem zeta_ratio_identity (s : ℂ) (hs : 1 < s.re) : riemannZeta (2 * s) / riemannZeta s = ∏' (p : ℙ), (1 + ↑↑p ^ (-s))⁻¹

theorem two_mul_ofReal_div_two (r : ℝ) : 2 * (↑r / 2) = ↑r

theorem zeta_ratio_identity_ofReal_div_two (r : ℝ) (hr : 1 < (↑r / 2).re) : riemannZeta ↑r / riemannZeta ↑(r / 2) = ∏' (p : ℙ), (1 + ↑↑p ^ (-(↑r / 2)))⁻¹

theorem zeta_ratio_at_3_2 : riemannZeta 3 / riemannZeta (↑3 / 2) = ∏' (p : ℙ), (1 + ↑↑p ^ (-(↑3 / 2)))⁻¹

theorem triangle_inequality_specific (z : ℂ) : ‖1 - z‖ ≤ 1 + ‖z‖

theorem re_neg_eq_neg_re (s : ℂ) : (-s).re = -s.re

theorem abs_cpow_eq_rpow_re_of_pos {x : ℝ} (hx : 0 < x) (y : ℂ) : ‖↑x ^ y‖ = x ^ y.re

theorem abs_p_pow_s (p : ℙ) (s : ℂ) : ‖↑↑p ^ (-s)‖ = ↑↑p ^ (-s.re)

theorem abs_term_bound (p : ℙ) (t : ℝ) : ‖1 - ↑↑p ^ (-(↑3 / 2 + ↑t * Complex.I))‖ ≤ 1 + ↑↑p ^ (-(3 / 2))

theorem inv_inequality {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : b⁻¹ ≤ a⁻¹

theorem eq_of_one_sub_eq_zero (z : ℂ) (h : 1 - z = 0) : z = 1

theorem condp32 (p : ℙ) (t : ℝ) : 1 - ↑↑p ^ (-(↑3 / 2 + ↑t * Complex.I)) ≠ 0

theorem abs_term_inv_bound (p : ℙ) (t : ℝ) : (1 + ↑↑p ^ (-(3 / 2)))⁻¹ ≤ ‖1 - ↑↑p ^ (-(↑3 / 2 + ↑t * Complex.I))‖⁻¹

theorem prod_inequality {P : Type u_1} (a b : P → NNReal) (ha : Multipliable a) (hb : Multipliable b) (hab : ∀ (p : P), a p ≤ b p) : ∏' (p : P), a p ≤ ∏' (p : P), b p

theorem multipliable_complex_abs_inv {i : Type u_1} (g : i → ℂ) (h_mult : Multipliable fun (i : i) => (1 - g i)⁻¹) (h_nonzero : ∀ (i : i), 1 - g i ≠ 0) : Multipliable fun (i : i) => ‖1 - g i‖⁻¹

theorem multipliable_positive_inv_powers (r : ℝ) (hr : 1 < r) : Multipliable fun (p : ℙ) => (1 + ↑↑p ^ (-r))⁻¹

theorem hasProd_map_nnreal_coe {i : Type u_1} (f : i → NNReal) (a : NNReal) (h : HasProd f a) : HasProd (fun (i : i) => ↑(f i)) ↑a

theorem multipliable_nnreal_coe {i : Type u_1} (f : i → NNReal) (hf : Multipliable f) : Multipliable fun (i : i) => ↑(f i)

theorem nnreal_coe_tprod_eq {i : Type u_1} (f : i → NNReal) (hf : Multipliable f) : ∏' (i : i), ↑(f i) = ∏' (i : i), ↑(f i)

theorem hasProd_nonneg_of_pos {i : Type u_1} (f : i → ℝ) (hpos : ∀ (i : i), 0 < f i) (a : ℝ) (ha : HasProd f a) : 0 ≤ a

theorem tendsto_finprod_coe_iff_tendsto_coe_finprod {i : Type u_1} (f : i → NNReal) (a : NNReal) : Filter.Tendsto (fun (s : Finset i) => ∏ i ∈ s, ↑(f i)) Filter.atTop (nhds ↑a) ↔ Filter.Tendsto ((fun (x : NNReal) => ↑x) ∘ fun (s : Finset i) => ∏ i ∈ s, f i) Filter.atTop (nhds ↑a)

theorem NNReal.isEmbedding_coe : Topology.IsEmbedding fun (x : NNReal) => ↑x

theorem HasProd.of_coe_hasProd {i : Type u_1} (f : i → NNReal) (a : NNReal) (h : HasProd (fun (i : i) => ↑(f i)) ↑a) : HasProd f a

theorem hasProd_nnreal_of_coe {i : Type u_1} (g : i → NNReal) (b : NNReal) (h : HasProd (fun (i : i) => ↑(g i)) ↑b) : HasProd g b

theorem multipliable_real_to_nnreal {i : Type u_1} (f : i → ℝ) (hpos : ∀ (i : i), 0 < f i) (h_mult : Multipliable f) : Multipliable fun (i : i) => ⟨f i, ⋯⟩

theorem nnreal_coe_tprod_eq_tprod_coe {i : Type u_1} (f : i → NNReal) (hf : Multipliable f) : ∏' (i : i), ↑(f i) = ↑(∏' (i : i), f i)

theorem nnreal_tprod_le_coe {i : Type u_1} (f g : i → NNReal) (hf : Multipliable f) (hg : Multipliable g) (h : ∏' (i : i), f i ≤ ∏' (i : i), g i) : ∏' (i : i), ↑(f i) ≤ ∏' (i : i), ↑(g i)

theorem abs_zeta_inequality (t : ℝ) : ∏' (p : ℙ), (1 + ↑↑p ^ (-(3 / 2)))⁻¹ ≤ ∏' (p : ℙ), ‖1 - ↑↑p ^ (-(↑3 / 2 + ↑t * Complex.I))‖⁻¹

theorem abs_zeta_ratio_eval : ‖riemannZeta 3 / riemannZeta (↑3 / 2)‖ = ∏' (p : ℙ), (1 + ↑↑p ^ (-(3 / 2)))⁻¹

theorem zeta_lower_bound (t : ℝ) : ‖riemannZeta 3 / riemannZeta (↑3 / 2)‖ ≤ ‖riemannZeta (↑3 / 2 + ↑t * Complex.I)‖

theorem summable_one_div_nat_add_rpow' {x : ℝ} (hx : 1 < x) : Summable fun (n : ℕ) => 1 / (↑n + 1) ^ x

theorem tsum_pos_of_pos_first_term {f : ℕ → ℝ} (hf : Summable f) (h0 : 0 < f 0) (hnonneg : ∀ (n : ℕ), 0 ≤ f n) : 0 < ∑' (n : ℕ), f n

theorem first_term_pos (x : ℝ) : 0 < 1 / 1 ^ x

theorem terms_nonneg (x : ℝ) (n : ℕ) : 0 ≤ 1 / (↑n + 1) ^ x

theorem term_eq_ofRealC (x : ℝ) (n : ℕ) : 1 / (↑n + 1) ^ ↑x = ↑(1 / (↑n + 1) ^ x)

theorem zeta_eq_ofReal (x : ℝ) (hx : 1 < x) : riemannZeta ↑x = ↑(∑' (n : ℕ), 1 / (↑n + 1) ^ x)

theorem term_inv_eq_ofRealC (x : ℝ) (n : ℕ) : ((↑n + 1) ^ ↑x)⁻¹ = ↑(1 / (↑n + 1) ^ x)

theorem im_tsum_ofReal (g : ℕ → ℝ) : (∑' (n : ℕ), ↑(g n)).im = 0

theorem re_tsum_ofReal (g : ℕ → ℝ) : (∑' (n : ℕ), ↑(g n)).re = ∑' (n : ℕ), g n

theorem zetapos (x : ℝ) (hx : 1 < x) : (riemannZeta ↑x).im = 0 ∧ 0 < (riemannZeta ↑x).re

theorem zeta332pos : 0 < ‖riemannZeta 3 / riemannZeta (↑3 / 2)‖

theorem zeta_low_332 : ∃ (a : ℝ), 0 < a ∧ ∀ (t : ℝ), a ≤ ‖riemannZeta (↑3 / 2 + ↑t * Complex.I)‖

theorem one_div_nat_cpow_eq_ite_cpow_neg (s : ℂ) (hs : s ≠ 0) (n : ℕ) : 1 / ↑n ^ s = if n = 0 then 0 else ↑n ^ (-s)

theorem lem_zetaLimit (s : ℂ) (hs : 1 < s.re) : riemannZeta s = ∑' (n : ℕ), if n = 0 then 0 else ↑n ^ (-s)

Lemma 1: Basic zeta function series representation.

noncomputable def zetaPartialSum (s : ℂ) (N : ℕ) : ℂ

Definition: Partial sum of zeta.

Equations

• zetaPartialSum s N = ∑ n ∈ Finset.range N, (↑n + 1) ^ (-s)

theorem sum_Icc1_eq_sum_range_succ (N : ℕ) (g : ℕ → ℂ) : ∑ k ∈ Finset.Icc 1 N, g k = ∑ n ∈ Finset.range N, g (n + 1)

theorem sum_Icc0_eq_sum_Icc1_of_zero (N : ℕ) (g : ℕ → ℂ) (h0 : g 0 = 0) : ∑ k ∈ Finset.Icc 0 N, g k = ∑ k ∈ Finset.Icc 1 N, g k

theorem sum_Icc0_shifted_eq_sum_range (a : ℕ → ℂ) (m : ℕ) : (∑ k ∈ Finset.Icc 0 m, if k = 0 then 0 else a k) = ∑ n ∈ Finset.range m, a (n + 1)

theorem sum_Icc0_shifted_floor_eq (a : ℕ → ℂ) (t : ℝ) : (∑ k ∈ Finset.Icc 0 ⌊t⌋₊, if k = 0 then 0 else a k) = ∑ n ∈ Finset.range ⌊t⌋₊, a (n + 1)

theorem helper_contdiff_differentiable_integrable (f : ℝ → ℂ) (hf : ContDiff ℝ 1 f) (a b : ℝ) : (∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) ∧ MeasureTheory.IntegrableOn (deriv f) (Set.Icc a b) MeasureTheory.volume

theorem sum_range_mul_shift_comm (N : ℕ) (a : ℕ → ℂ) (f : ℝ → ℂ) : (∑ n ∈ Finset.range N, f (↑n + 1) * if n + 1 = 0 then 0 else a (n + 1)) = ∑ n ∈ Finset.range N, a (n + 1) * f (↑n + 1)

theorem sum_range_shifted_coeffs (N : ℕ) (a c : ℕ → ℂ) (f : ℝ → ℂ) (hshift : ∀ (n : ℕ), c (n + 1) = a (n + 1)) : ∑ n ∈ Finset.range N, f ↑(n + 1) * c (n + 1) = ∑ n ∈ Finset.range N, f ↑(n + 1) * a (n + 1)

theorem sum_range_commute_mul (N : ℕ) (a : ℕ → ℂ) (f : ℝ → ℂ) : ∑ n ∈ Finset.range N, f ↑(n + 1) * a (n + 1) = ∑ n ∈ Finset.range N, a (n + 1) * f ↑(n + 1)

theorem lem_abelSummation {a : ℕ → ℂ} {f : ℝ → ℂ} (hf : ContDiff ℝ 1 f) (N : ℕ) (hN : 1 ≤ N) : let A := fun (u : ℝ) => ∑ n ∈ Finset.range ⌊u⌋₊, a (n + 1); ∑ n ∈ Finset.range N, a (n + 1) * f (↑n + 1) = A ↑N * f ↑N - ∫ (u : ℝ) in 1 ..↑N, A u * deriv f u

theorem lem_partialSumIsZetaN (s : ℂ) (N : ℕ) : let f := fun (u : ℝ) => ↑u ^ (-s); let a := fun (_n : ℕ) => 1; zetaPartialSum s N = ∑ n ∈ Finset.range N, a n * f (↑n + 1)

Lemma: Partial sum equals ∑ a(n) f(n+1) with a(n)=1, f(u)=u^{-s}.

theorem lem_sumOfAn (u : ℝ) (hu : 1 ≤ u) : let a := fun (_n : ℕ) => 1; let A := fun (u : ℝ) => ∑ n ∈ Finset.range ⌊u⌋₊, a (n + 1); A u = ↑⌊u⌋₊

Lemma: Sum of a_n = 1.

theorem lem_fDeriv (s : ℂ) (u : ℝ) (hu : 0 < u) : let f := fun (u : ℝ) => ↑u ^ (-s); deriv f u = -s * ↑u ^ (-s - 1)

Lemma: Derivative of f(u)=u^{-s}.

theorem differentiable_integrable_cpow_on_Icc (s : ℂ) (a b : ℝ) (h0 : 0 < a) (hle : a ≤ b) : (∀ t ∈ Set.Icc a b, DifferentiableAt ℝ (fun (u : ℝ) => ↑u ^ (-s)) t) ∧ MeasureTheory.IntegrableOn (deriv fun (u : ℝ) => ↑u ^ (-s)) (Set.Icc a b) MeasureTheory.volume

theorem intervalIntegral_congr_of_Ioc_eq (a b : ℝ) (h : a ≤ b) (f g : ℝ → ℂ) (hpt : ∀ u ∈ Set.Ioc a b, f u = g u) : ∫ (u : ℝ) in a..b, f u = ∫ (u : ℝ) in a..b, g u

theorem lem_applyAbel (s : ℂ) (N : ℕ) (hN : 1 ≤ N) : zetaPartialSum s N = ↑N * ↑N ^ (-s) - ∫ (u : ℝ) in 1 ..↑N, ↑⌊u⌋₊ * (-s * ↑u ^ (-s - 1))

Lemma: Apply Abel with a_n=1, f(u)=u^{-s}.

theorem lem_floorNisN (N : ℕ) (hN : 1 ≤ N) : ⌊↑N⌋₊ = N

Lemma: Nat.floor (N : ℝ) = N for natural N.

theorem helper_integral_const_mul (a b : ℝ) (c : ℂ) (g : ℝ → ℂ) : ∫ (x : ℝ) in a..b, c * g x = c * ∫ (x : ℝ) in a..b, g x

theorem helper_cpow_mul_cpow_neg_eq_cpow_sub (x s : ℂ) (hx : x ≠ 0) : x * x ^ (-s) = x ^ (1 - s)

theorem lem_zetaNsimplified1 (s : ℂ) (N : ℕ) (hN : 1 ≤ N) : zetaPartialSum s N = ↑N ^ (1 - s) + s * ∫ (u : ℝ) in 1 ..↑N, ↑⌊u⌋₊ * ↑u ^ (-s - 1)

Lemma: Simplified ζ_N formula 1.

theorem lem_floorUdecomp (u : ℝ) : ↑⌊u⌋ = u - Int.fract u

Lemma: Floor decomposition using fractional part.

theorem lem_fracPartBound (u : ℝ) : 0 ≤ Int.fract u ∧ Int.fract u < 1 ∧ |Int.fract u| ≤ 1

Lemma: Fractional part bound.

theorem helper_continuousOn_cpow (r : ℂ) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : ContinuousOn (fun (u : ℝ) => ↑u ^ r) (Set.Icc a b)

Helper: continuity of u ↦ (u:ℂ)^r on Icc a b when a>0.

theorem helper_intervalIntegrable_mul_cpow_id (s : ℂ) {a b : ℝ} (ha : 1 ≤ a) (hab : a ≤ b) : IntervalIntegrable (fun (u : ℝ) => ↑u * ↑u ^ (-s - 1)) MeasureTheory.volume a b

Helper: IntervalIntegrable of (u:ℂ)*(u:ℂ)^(-s-1) on [a,b] when a≥1.

theorem helper_aestronglyMeasurable_kernel_Icc (s : ℂ) {a b : ℝ} : MeasureTheory.AEStronglyMeasurable (fun (u : ℝ) => ↑(Int.fract u) * ↑u ^ (-s - 1)) (MeasureTheory.volume.restrict (Set.Icc a b))

Helper: a.e.-strong measurability for the fractional-part kernel on Icc.

theorem helper_intervalIntegrable_frac_kernel (s : ℂ) {a b : ℝ} (ha : 1 ≤ a) (hab : a ≤ b) : IntervalIntegrable (fun (u : ℝ) => ↑(Int.fract u) * ↑u ^ (-s - 1)) MeasureTheory.volume a b

Helper: IntervalIntegrable of the fractional-part kernel on [a,b] when a≥1.

theorem lem_integralSplit (s : ℂ) (N : ℕ) (hN : 1 ≤ N) : ∫ (u : ℝ) in 1 ..↑N, ↑⌊u⌋₊ * ↑u ^ (-s - 1) = (∫ (u : ℝ) in 1 ..↑N, ↑u ^ (-s)) - ∫ (u : ℝ) in 1 ..↑N, ↑(Int.fract u) * ↑u ^ (-s - 1)

Lemma: Integral split using floor = u - fract.

theorem lem_zetaNsimplified2 (s : ℂ) (N : ℕ) (hN : 1 ≤ N) : zetaPartialSum s N = (↑N ^ (1 - s) + s * ∫ (u : ℝ) in 1 ..↑N, ↑u ^ (-s)) - s * ∫ (u : ℝ) in 1 ..↑N, ↑(Int.fract u) * ↑u ^ (-s - 1)

Lemma: Simplified ζ_N formula 2.

theorem lem_evalMainIntegral (s : ℂ) (hs : s ≠ 1) (N : ℕ) (hN : 1 ≤ N) : s * ∫ (u : ℝ) in 1 ..↑N, ↑u ^ (-s) = s / (1 - s) * (↑N ^ (1 - s) - 1)

Lemma: Evaluate the main integral.

theorem lem_zetaNfinal (s : ℂ) (hs : s ≠ 1) (N : ℕ) (hN : 1 ≤ N) : zetaPartialSum s N = ↑N ^ (1 - s) / (1 - s) + 1 + 1 / (s - 1) - s * ∫ (u : ℝ) in 1 ..↑N, ↑(Int.fract u) * ↑u ^ (-s - 1)

Lemma: Final ζ_N formula.

theorem complex_tendsto_zero_iff_norm_tendsto_zero {α : Type u_1} {f : α → ℂ} {l : Filter α} : Filter.Tendsto f l (nhds 0) ↔ Filter.Tendsto (fun (x : α) => ‖f x‖) l (nhds 0)

theorem complex_norm_natCast_cpow (N : ℕ) (w : ℂ) (hN : 0 < N) : ‖↑N ^ w‖ = ↑N ^ w.re

theorem tendsto_natCast_cpow_zero_of_neg_re (w : ℂ) (hw : w.re < 0) : Filter.Tendsto (fun (N : ℕ) => ↑N ^ w) Filter.atTop (nhds 0)

theorem lem_limitTerm1 (s : ℂ) (hs : 1 < s.re) : Filter.Tendsto (fun (N : ℕ) => ↑N ^ (1 - s)) Filter.atTop (nhds 0)

theorem lem_integrandBound (u : ℝ) (hu : 1 ≤ u) (s : ℂ) : ‖↑(Int.fract u) * ↑u ^ (-s - 1)‖ ≤ u ^ (-s.re - 1)

Lemma: Integrand bound.

theorem lem_integrandBoundeps (ε : ℝ) (hε : 0 < ε) (u : ℝ) (hu : 1 ≤ u) (s : ℂ) (hs : ε ≤ s.re) : ‖↑(Int.fract u) * ↑u ^ (-s - 1)‖ ≤ u ^ (-1 - ε)

Lemma: Integrand bound with ε.

theorem lem_triangleInequality_add (z₁ z₂ : ℂ) : ‖z₁ + z₂‖ ≤ ‖z₁‖ + ‖z₂‖

Lemma: Triangle inequality (scalar and integral versions).

theorem lem_triangleInequality_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (h : a ≤ b) : ‖∫ (u : ℝ) in a..b, f u‖ ≤ ∫ (u : ℝ) in a..b, ‖f u‖

theorem helper_integral_interval_sub_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b c : ℝ} (hab : IntervalIntegrable f MeasureTheory.volume a b) (hac : IntervalIntegrable f MeasureTheory.volume a c) : (∫ (x : ℝ) in a..b, f x) - ∫ (x : ℝ) in a..c, f x = ∫ (x : ℝ) in c..b, f x

Lemma: Integral convergence of the fractional-part kernel.

theorem helper_integral_rpow_eval {ε : ℝ} (hε : 0 < ε) {m n : ℝ} (hm : 1 ≤ m) (hmn : m ≤ n) : ∫ (u : ℝ) in m..n, u ^ (-1 - ε) = (m ^ (-ε) - n ^ (-ε)) / ε

theorem helper_integral_rpow_le {ε : ℝ} (hε : 0 < ε) {m n : ℝ} (hm : 1 ≤ m) (hmn : m ≤ n) : ∫ (u : ℝ) in m..n, u ^ (-1 - ε) ≤ 1 / ε * m ^ (-ε)

theorem helper_tendsto_nat_rpow_neg (ε : ℝ) (hε : 0 < ε) : Filter.Tendsto (fun (m : ℕ) => ↑m ^ (-ε)) Filter.atTop (nhds 0)

theorem helper_exists_limit_of_tail_bound (a : ℕ → ℂ) (b : ℕ → ℝ) (hb_nonneg : ∀ (m : ℕ), 0 ≤ b m) (hb_tendsto : Filter.Tendsto b Filter.atTop (nhds 0)) (hbound : ∀ᶠ (m : ℕ) (n : ℕ) in Filter.atTop, m ≤ n → ‖a n - a m‖ ≤ b m) : ∃ (l : ℂ), Filter.Tendsto a Filter.atTop (nhds l)

theorem helper_limit_norm_le_of_uniform_bound {a : ℕ → ℂ} {l : ℂ} {B : ℝ} (h : Filter.Tendsto a Filter.atTop (nhds l)) (hbound : ∀ (n : ℕ), ‖a n‖ ≤ B) : ‖l‖ ≤ B

theorem helper_one_le_of_mem_Icc {m n u : ℝ} (hm : 1 ≤ m) (hu : u ∈ Set.Icc m n) : 1 ≤ u

theorem helper_intervalIntegrable_rpow_neg {ε a b : ℝ} (hε : 0 < ε) (ha : 1 ≤ a) (hab : a ≤ b) : IntervalIntegrable (fun (u : ℝ) => u ^ (-1 - ε)) MeasureTheory.volume a b

theorem helper_one_le_of_mem_Ioc {m n u : ℝ} (hm : 1 ≤ m) (hu : u ∈ Set.Ioc m n) : 1 ≤ u

theorem helper_integrableOn_of_bound_Ioc {m n : ℝ} {f : ℝ → ℂ} {g : ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioc m n))) (hbound : ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc m n), ‖f u‖ ≤ g u) (hg : MeasureTheory.IntegrableOn g (Set.Ioc m n) MeasureTheory.volume) : MeasureTheory.IntegrableOn f (Set.Ioc m n) MeasureTheory.volume

theorem helper_aestronglyMeasurable_kernel_Ioc (s : ℂ) {m n : ℝ} : MeasureTheory.AEStronglyMeasurable (fun (u : ℝ) => ↑(Int.fract u) * ↑u ^ (-s - 1)) (MeasureTheory.volume.restrict (Set.Ioc m n))

theorem helper_aebound_kernel_Ioc {ε : ℝ} (hε : 0 < ε) (s : ℂ) (hs : ε ≤ s.re) {m n : ℝ} (hm : 1 ≤ m) (hmn : m ≤ n) : ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc m n), ‖↑(Int.fract u) * ↑u ^ (-s - 1)‖ ≤ u ^ (-1 - ε)

theorem helper_integrableOn_rpow_neg_Ioc {ε : ℝ} (hε : 0 < ε) {m n : ℝ} (hm : 1 ≤ m) (hmn : m ≤ n) : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ (-1 - ε)) (Set.Ioc m n) MeasureTheory.volume

theorem helper_intervalIntegrable_of_integrableOn_Ioc {f : ℝ → ℂ} {m n : ℝ} (hmn : m ≤ n) (hint : MeasureTheory.IntegrableOn f (Set.Ioc m n) MeasureTheory.volume) : IntervalIntegrable f MeasureTheory.volume m n

theorem helper_rpow_neg_nonneg_on {ε a b : ℝ} (hε : 0 < ε) (ha : 1 ≤ a) (hab : a ≤ b) (u : ℝ) : u ∈ Set.Icc a b → 0 ≤ u ^ (-1 - ε)

theorem helper_norm_integral_le_integral_norm_of_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (h : a ≤ b) : ‖∫ (u : ℝ) in a..b, f u‖ ≤ ∫ (u : ℝ) in a..b, ‖f u‖

theorem helper_tendsto_const_mul_zero (c : ℝ) {f : ℕ → ℝ} (h : Filter.Tendsto f Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => c * f n) Filter.atTop (nhds 0)

theorem helper_limit_norm_le_of_eventual_bound {a : ℕ → ℂ} {l : ℂ} {B : ℝ} (h : Filter.Tendsto a Filter.atTop (nhds l)) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, ‖a n‖ ≤ B) : ‖l‖ ≤ B

theorem lem_integralConvergence (ε : ℝ) (hε : 0 < ε) (s : ℂ) (hs : ε ≤ s.re) : ∃ (I : ℂ), Filter.Tendsto (fun (N : ℕ) => ∫ (u : ℝ) in 1 ..↑N, ↑(Int.fract u) * ↑u ^ (-s - 1)) Filter.atTop (nhds I) ∧ ‖I‖ ≤ 1 / ε

theorem helper_tendsto_zetaPartialSum_to_zeta (s : ℂ) (hs : 1 < s.re) : Filter.Tendsto (fun (N : ℕ) => zetaPartialSum s N) Filter.atTop (nhds (riemannZeta s))

Lemma: Zeta formula for Re(s) > 1.

theorem integrableOn_of_ae_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {g : ℝ → ℝ} {s : Set ℝ} (hfm : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict s)) (hgint : MeasureTheory.IntegrableOn g s MeasureTheory.volume) (hbound : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict s, ‖f x‖ ≤ g x) : MeasureTheory.IntegrableOn f s MeasureTheory.volume

theorem kernel_aestronglyMeasurable_on_Ioi (s : ℂ) (a : ℝ) : MeasureTheory.AEStronglyMeasurable (fun (u : ℝ) => ↑(Int.fract u) * ↑u ^ (-s - 1)) (MeasureTheory.volume.restrict (Set.Ioi a))

theorem kernel_ae_bound_on_Ioi (s : ℂ) : ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 1), ‖↑(Int.fract u) * ↑u ^ (-s - 1)‖ ≤ u ^ (-s.re - 1)

theorem helper_intervalIntegral_tendstoIoi_kernel (s : ℂ) (hs : 1 < s.re) : Filter.Tendsto (fun (N : ℕ) => ∫ (u : ℝ) in 1 ..↑N, ↑(Int.fract u) * ↑u ^ (-s - 1)) Filter.atTop (nhds (∫ (u : ℝ) in Set.Ioi 1, ↑(Int.fract u) * ↑u ^ (-s - 1)))

theorem helper_zetaNfinal (s : ℂ) (hs : s ≠ 1) (N : ℕ) (hN : 1 ≤ N) : zetaPartialSum s N = ↑N ^ (1 - s) / (1 - s) + 1 + 1 / (s - 1) - s * ∫ (u : ℝ) in 1 ..↑N, ↑(Int.fract u) * ↑u ^ (-s - 1)

theorem helper_eventually_eq_from_zetaNfinal (s : ℂ) (hs : s ≠ 1) : ∀ᶠ (N : ℕ) in Filter.atTop, zetaPartialSum s N = ↑N ^ (1 - s) / (1 - s) + 1 + 1 / (s - 1) - s * ∫ (u : ℝ) in 1 ..↑N, ↑(Int.fract u) * ↑u ^ (-s - 1)

theorem helper_limit_scaled_cpow (s : ℂ) (hs : 1 < s.re) (hsne : s ≠ 1) : Filter.Tendsto (fun (N : ℕ) => ↑N ^ (1 - s) / (1 - s)) Filter.atTop (nhds 0)

theorem helper_tendsto_const_mul {f : ℕ → ℂ} {l : ℂ} (c : ℂ) (h : Filter.Tendsto f Filter.atTop (nhds l)) : Filter.Tendsto (fun (n : ℕ) => c * f n) Filter.atTop (nhds (c * l))

theorem helper_tendsto_add {f g : ℕ → ℂ} {a b : ℂ} (hf : Filter.Tendsto f Filter.atTop (nhds a)) (hg : Filter.Tendsto g Filter.atTop (nhds b)) : Filter.Tendsto (fun (n : ℕ) => f n + g n) Filter.atTop (nhds (a + b))

theorem helper_tendsto_neg {f : ℕ → ℂ} {a : ℂ} (hf : Filter.Tendsto f Filter.atTop (nhds a)) : Filter.Tendsto (fun (n : ℕ) => -f n) Filter.atTop (nhds (-a))

theorem helper_tendsto_sub {f g : ℕ → ℂ} {a b : ℂ} (hf : Filter.Tendsto f Filter.atTop (nhds a)) (hg : Filter.Tendsto g Filter.atTop (nhds b)) : Filter.Tendsto (fun (n : ℕ) => f n - g n) Filter.atTop (nhds (a - b))

theorem lem_zetaFormula (s : ℂ) (hs : 1 < s.re) : riemannZeta s = 1 + 1 / (s - 1) - s * ∫ (u : ℝ) in Set.Ioi 1, ↑(Int.fract u) * ↑u ^ (-s - 1)

theorem lem_zetaanalOnnot1 : AnalyticOn ℂ riemannZeta {s : ℂ | s ≠ 1}

theorem lem_zetaanalS : let S := {s : ℂ | s ≠ 1}; AnalyticOn ℂ riemannZeta S

Lemma: Zeta is analytic on ℂ \ {1}.

theorem lem_S_isOpen : let S := {s : ℂ | s ≠ 1}; IsOpen S

Lemma: The set S = {s : ℂ | s ≠ 1} is open.

theorem lem_T_isOpen : let S := {s : ℂ | s ≠ 1}; let T := {s : ℂ | s ∈ S ∧ 1 / 10 < s.re}; IsOpen T

Lemma: The set T = {s ∈ S | Re(s) > 1/10} is open.

theorem helper_T_open : let S := {s : ℂ | s ≠ 1}; let T := {s : ℂ | s ∈ S ∧ 1 / 10 < s.re}; IsOpen T

theorem open_mem_interior_of_isOpen {X : Type u_1} [TopologicalSpace X] {U : Set X} (hU : IsOpen U) {x : X} (hx : x ∈ U) : x ∈ interior U

theorem isOpen_halfplane_re_gt (a : ℝ) : IsOpen {z : ℂ | a < z.re}

theorem T_eq_inter_S_half (S T : Set ℂ) (hS : S = {s : ℂ | s ≠ 1}) (hT : T = {s : ℂ | s ∈ S ∧ 1 / 10 < s.re}) : T = S ∩ {s : ℂ | 1 / 10 < s.re}

theorem inter_compl_singleton_eq_diff {α : Type u_1} [DecidableEq α] (A : Set α) (x : α) : A ∩ {x}ᶜ = A \ {x}

theorem joinedIn_of_path_forall_mem {s : Set ℂ} {x y : ℂ} (γ : Path x y) (hγ : ∀ (t : ↑unitInterval), γ t ∈ s) : JoinedIn s x y

theorem path_forall_mem_symm {x y : ℂ} {P : ℂ → Prop} (γ : Path x y) (h : ∀ (t : ↑unitInterval), P (γ t)) (t : ↑unitInterval) : P (γ.symm t)

theorem isPathConnected_punctured_halfplane_re_gt (a : ℝ) (p : ℂ) (hp : a < p.re) : IsPathConnected ({z : ℂ | a < z.re} \ {p})

theorem inter_compl_singleton_eq_diff' {α : Type u_1} [DecidableEq α] (A : Set α) (x : α) : A ∩ {x}ᶜ = A \ {x}

theorem lem_T_isPreconnected : let S := {s : ℂ | s ≠ 1}; let T := {s : ℂ | s ∈ S ∧ 1 / 10 < s.re}; IsPreconnected T

Lemma: The set T = {s ∈ S | Re(s) > 1/10} is preconnected.

theorem hasDerivAt_param_cpow_neg_one (u : ℝ) (hu : 0 < u) (z : ℂ) : HasDerivAt (fun (w : ℂ) => ↑u ^ (-w - 1)) (-↑(Real.log u) * ↑u ^ (-z - 1)) z

theorem integrableOn_t_mul_exp_neg (ε : ℝ) (hε : 0 < ε) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t * Real.exp (-ε * t)) (Set.Ioi 0) MeasureTheory.volume

theorem aestronglyMeasurable_kernel_param_deriv (z : ℂ) : MeasureTheory.AEStronglyMeasurable (fun (u : ℝ) => -↑(Real.log u) * (↑(Int.fract u) * ↑u ^ (-z - 1))) (MeasureTheory.volume.restrict (Set.Ioi 1))

theorem kernel_deriv_norm_bound_on_ball (ε u : ℝ) (hu : 1 < u) (x : ℂ) (hx : ε ≤ x.re) : ‖-↑(Real.log u) * (↑(Int.fract u) * ↑u ^ (-x - 1))‖ ≤ Real.log u * u ^ (-1 - ε)

theorem exists_radius_ball_two_step_subset_halfspace (s : ℂ) {ε : ℝ} (hε : ε < s.re) : ∃ δ > 0, ∀ (x : ℂ), dist x s < δ → ∀ (y : ℂ), dist y x < δ → ε ≤ y.re

theorem integrable_kernel_at_param (s : ℂ) (hs : 0 < s.re) : MeasureTheory.Integrable (fun (u : ℝ) => ↑(Int.fract u) * ↑u ^ (-s - 1)) (MeasureTheory.volume.restrict (Set.Ioi 1))

theorem eventually_aestronglyMeasurable_kernel_param (s : ℂ) : ∀ᶠ (z : ℂ) in nhds s, MeasureTheory.AEStronglyMeasurable (fun (u : ℝ) => ↑(Int.fract u) * ↑u ^ (-z - 1)) (MeasureTheory.volume.restrict (Set.Ioi 1))

theorem hasDerivAt_kernel_in_param (u : ℝ) (hu : 1 < u) (z : ℂ) : HasDerivAt (fun (w : ℂ) => ↑(Int.fract u) * ↑u ^ (-w - 1)) (-↑(Real.log u) * (↑(Int.fract u) * ↑u ^ (-z - 1))) z

theorem hasDerivAt_integral_param_dominated_Ioi (F F' : ℂ → ℝ → ℂ) (s : ℂ) (δ : ℝ) (hδ : 0 < δ) (hmeas : ∀ᶠ (z : ℂ) in nhds s, MeasureTheory.AEStronglyMeasurable (F z) (MeasureTheory.volume.restrict (Set.Ioi 1))) (hFint : MeasureTheory.Integrable (F s) (MeasureTheory.volume.restrict (Set.Ioi 1))) (hF'meas : MeasureTheory.AEStronglyMeasurable (F' s) (MeasureTheory.volume.restrict (Set.Ioi 1))) (bound : ℝ → ℝ) (hbound_int : MeasureTheory.Integrable bound (MeasureTheory.volume.restrict (Set.Ioi 1))) (hbound : ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 1), ∀ z ∈ Metric.ball s δ, ‖F' z u‖ ≤ bound u) (hderiv : ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 1), ∀ z ∈ Metric.ball s δ, HasDerivAt (fun (w : ℂ) => F w u) (F' z u) z) : HasDerivAt (fun (z : ℂ) => ∫ (u : ℝ) in Set.Ioi 1, F z u) (∫ (u : ℝ) in Set.Ioi 1, F' s u) s

theorem dist_lt_of_mem_two_balls {x z s : ℂ} {r : ℝ} (hxz : dist x z < r) (hzs : dist z s < r) : dist x s < r + r

theorem mem_ball_of_mem_two_half_balls {x z s : ℂ} {δ : ℝ} (hx : x ∈ Metric.ball z (δ / 2)) (hz : z ∈ Metric.ball s (δ / 2)) : x ∈ Metric.ball s δ

theorem dist_lt_delta_of_half {x s : ℂ} {δ : ℝ} (hδpos : 0 < δ) (hx : dist x s < δ / 2) : dist x s < δ

theorem re_lower_bound_from_two_step {s x : ℂ} {ε δ : ℝ} (h : ∀ (z : ℂ), dist z s < δ → ∀ (y : ℂ), dist y z < δ → ε ≤ y.re) (hδpos : 0 < δ) (hx : dist x s < δ) : ε ≤ x.re

theorem analyticAt_of_eventually_differentiableAt {f : ℂ → ℂ} {s : ℂ} (h : ∀ᶠ (z : ℂ) in nhds s, DifferentiableAt ℂ f z) : AnalyticAt ℂ f s

theorem kernel_integrable_param_of_re_pos (z : ℂ) (hz : 0 < z.re) : MeasureTheory.Integrable (fun (u : ℝ) => ↑(Int.fract u) * ↑u ^ (-z - 1)) (MeasureTheory.volume.restrict (Set.Ioi 1))

theorem integrable_kernel_at_param' (z : ℂ) (hz : 0 < z.re) : MeasureTheory.Integrable (fun (u : ℝ) => ↑(Int.fract u) * ↑u ^ (-z - 1)) (MeasureTheory.volume.restrict (Set.Ioi 1))

theorem lem_integralAnalytic (s : ℂ) (hs : 1 / 10 < s.re) : AnalyticAt ℂ (fun (z : ℂ) => ∫ (u : ℝ) in Set.Ioi 1, ↑(Int.fract u) * ↑u ^ (-z - 1)) s

theorem lem_zetaFormulaAC : let S := {s : ℂ | s ≠ 1}; let T := {s : ℂ | s ∈ S ∧ 1 / 10 < s.re}; let F := fun (z : ℂ) => z / (z - 1) - z * ∫ (u : ℝ) in Set.Ioi 1, ↑(Int.fract u) * ↑u ^ (-z - 1); AnalyticOn ℂ F T

Lemma: The continuation formula is analytic on T = { s ≠ 1, Re(s) > 0 }.

theorem lem_div_eq_one_plus_one_div (z : ℂ) (hz : z ≠ 1) : z / (z - 1) = 1 + 1 / (z - 1)

Lemma: Algebraic identity for complex division.

theorem lem_zetaAnalyticContinuation : let S := {s : ℂ | s ≠ 1}; let T := {s : ℂ | s ∈ S ∧ 1 / 10 < s.re}; ∀ s ∈ T, riemannZeta s = 1 + 1 / (s - 1) - s * ∫ (u : ℝ) in Set.Ioi 1, ↑(Int.fract u) * ↑u ^ (-s - 1)

Lemma: Analytic continuation identity on T = { s ≠ 1, Re(s) > 0 }.

theorem lem_zetaBound1 (s : ℂ) (hs_re : 1 / 10 < s.re) (hs_ne : s ≠ 1) : ‖riemannZeta s‖ ≤ 1 + ‖1 / (s - 1)‖ + ‖s‖ * ‖∫ (u : ℝ) in Set.Ioi 1, ↑(Int.fract u) * ↑u ^ (-s - 1)‖

Lemma: Zeta bound 1 on Re(s) > 0, s ≠ 1.

theorem lem_integralBoundValue (s : ℂ) (hs : 0 < s.re) : ∫ (u : ℝ) in Set.Ioi 1, u ^ (-s.re - 1) = 1 / s.re

Lemma: Integral bound value ∫_{1}^{∞} u^{-Re(s)-1} = 1/Re(s).

theorem lem_zetaBound2 (s : ℂ) (hs_re : 1 / 10 < s.re) (hs_ne : s ≠ 1) : ‖riemannZeta s‖ ≤ 1 + ‖1 / (s - 1)‖ + ‖s‖ / s.re

Lemma: Zeta bound 2.

theorem lem_sOverSminus1Bound (s : ℂ) (hs : s ≠ 1) : ‖1 / (s - 1)‖ = 1 / ‖s - 1‖

Lemma: Reciprocal norm identity in ℂ.

theorem lem_zetaBound3 (s : ℂ) (hs_re : 1 / 10 < s.re) (hs_ne : s ≠ 1) : ‖riemannZeta s‖ ≤ 1 + 1 / ‖s - 1‖ + ‖s‖ / s.re

Lemma: Zeta bound 3.

theorem helper_normsq (z : ℂ) : ‖z‖ ^ 2 = z.re ^ 2 + z.im ^ 2

theorem helper_three_abs_sq (t : ℝ) : 3 ^ 2 + t ^ 2 ≤ (3 + |t|) ^ 2

theorem lem_sBound (s : ℂ) (hs : 1 / 2 ≤ s.re ∧ s.re < 3) : ‖s‖ < 3 + |s.im|

Lemma: Bound on ‖s‖ when 1/2 ≤ Re(s) < 3.

theorem lem_invReSbound (s : ℂ) (hs : 1 / 2 ≤ s.re ∧ s.re < 3) : 1 / s.re ≤ 2

Lemma: Bound on 1 / Re(s) under 1/2 ≤ Re(s) < 3.

theorem lem_invSminus1bound (s : ℂ) (hs_re : 1 / 2 ≤ s.re ∧ s.re < 3) (hs_im : 1 ≤ |s.im|) : 1 ≤ ‖s - 1‖

Lemma: Lower bound on ‖s - 1‖ when 1/2 ≤ Re(s) < 3 and |Im(s)| ≥ 1.

theorem reciprocal_le_one_of_one_le {x : ℝ} (hx_pos : 0 < x) (hx_ge : 1 ≤ x) : 1 / x ≤ 1

theorem div_le_mul_of_one_div_le {a c d : ℝ} (ha : 0 ≤ a) (hc : 0 < c) (h : 1 / c ≤ d) : a / c ≤ a * d

theorem lem_finalBoundCombination (s : ℂ) (hs_re : 1 / 2 ≤ s.re ∧ s.re < 3) (hs_im : 1 ≤ |s.im|) : ‖riemannZeta s‖ < 1 + 1 + (3 + |s.im|) * 2

Lemma: Final bound combination.

theorem lem_finalAlgebra (t : ℝ) : 1 + 1 + (3 + |t|) * 2 = 8 + 2 * |t|

Lemma: Final algebraic simplification.

theorem lem_zetaUppBd (z : ℂ) (hz_re : z.re ∈ Set.Ico (1 / 2) 3) (hz_im : 1 ≤ |z.im|) : ‖riemannZeta z‖ < 8 + 2 * |z.im|

Lemma: Upper bound on zeta in the vertical strip.

theorem lem_zfroms_calc (s : ℂ) (t : ℝ) : let z := s + ↑(3 / 2) + I * ↑t; z.re = s.re + 3 / 2 ∧ z.im = s.im + t

Lemma: z from s (first version).

theorem lem_zfroms_conditions (s : ℂ) (t : ℝ) (hs : ‖s‖ ≤ 1) (ht : 2 < |t|) : let z := s + ↑(3 / 2) + I * ↑t; z.re ∈ Set.Ico (1 / 2) 3 ∧ 1 ≤ |z.im|

theorem lem_abs_im_bound (s : ℂ) (t : ℝ) (hs : ‖s‖ ≤ 1) : |s.im + t| ≤ 1 + |t|

Helper lemma for the final bound.

theorem lem_zetaUppBound (t : ℝ) (s : ℂ) : ‖s‖ ≤ 1 → 2 < |t| → ‖riemannZeta (s + ↑(3 / 2) + I * ↑t)‖ < 10 + 2 * |t|

Lemma: Final zeta upper bound with shift.

noncomputable def logDerivZeta (s : ℂ) : ℂ

Equations

• logDerivZeta s = deriv riemannZeta s / riemannZeta s

def zerosetKfRc (R : ℝ) (c : ℂ) (f : ℂ → ℂ) : Set ℂ

Equations

• zerosetKfRc R c f = {ρ : ℂ | ρ ∈ Metric.closedBall c R ∧ f ρ = 0}

theorem zetadiffAtnot1 (s : ℂ) : s ≠ 1 → DifferentiableAt ℂ riemannZeta s

theorem DiffAtWithinAt {T : Set ℂ} {g : ℂ → ℂ} {s : ℂ} (_hs : s ∈ T) : DifferentiableAt ℂ g s → DifferentiableWithinAt ℂ g T s

theorem DiffWithinAtallOn {T : Set ℂ} {g : ℂ → ℂ} : (∀ s ∈ T, DifferentiableWithinAt ℂ g T s) → DifferentiableOn ℂ g T

theorem DiffAtOn {T : Set ℂ} {g : ℂ → ℂ} : (∀ s ∈ T, DifferentiableAt ℂ g s) → DifferentiableOn ℂ g T

theorem DiffOnanalOnNhd {T : Set ℂ} (hT : IsOpen T) {g : ℂ → ℂ} : DifferentiableOn ℂ g T → AnalyticOnNhd ℂ g T

theorem DiffAtallanalOnNhd {T : Set ℂ} (hT : IsOpen T) {g : ℂ → ℂ} : (∀ s ∈ T, DifferentiableAt ℂ g s) → AnalyticOnNhd ℂ g T

theorem zetaanalOnnot1 : AnalyticOnNhd ℂ riemannZeta {s : ℂ | s ≠ 1}

theorem I_mul_ofReal_im (t : ℝ) : (I * ↑t).im = t

theorem complex_im_sub_I_mul (a : ℂ) (t : ℝ) : (a - I * ↑t).im = a.im - t

theorem D1cinTt_pre (t : ℝ) (ht : |t| > 1) (s : ℂ) : s ∈ Metric.closedBall (3 / 2 + I * ↑t) 1 → s ≠ 1

theorem D1cinTt (t : ℝ) (ht : |t| > 1) : Metric.closedBall (3 / 2 + I * ↑t) 1 ⊆ {s : ℂ | s ≠ 1}

theorem zetaanalOnD1c (t : ℝ) (ht : |t| > 1) : AnalyticOnNhd ℂ riemannZeta (Metric.closedBall (3 / 2 + I * ↑t) 1)

theorem zetaanalOnD1c_general (x t : ℝ) (ht : |t| > 1) : AnalyticOnNhd ℂ riemannZeta (Metric.closedBall (↑x + I * ↑t) 1)

theorem sigmageq1 (s : ℂ) (hs : s.re > 1) : riemannZeta s ≠ 0

theorem Complex_I_mul_ofReal_re (r : ℝ) : (I * ↑r).re = 0

theorem re_real_add_I_mul_gt (a b : ℝ) (h : a > 1) : (↑a + I * ↑b).re > 1

theorem zetacnot0 (t : ℝ) : riemannZeta (3 / 2 + I * ↑t) ≠ 0

theorem zetacnot0_general (x t : ℝ) (hx : x > 1) : riemannZeta (↑x + I * ↑t) ≠ 0

theorem fc_analytic_normalized (c : ℂ) (f : ℂ → ℂ) (h_analytic : AnalyticOnNhd ℂ f (Metric.closedBall c 1)) (h_nonzero : f c ≠ 0) : AnalyticOnNhd ℂ (fun (z : ℂ) => f (z + c) / f c) (Metric.closedBall 0 1) ∧ (fun (z : ℂ) => f (z + c) / f c) 0 = 1

theorem deriv_normalized_nohd (c : ℂ) (f : ℂ → ℂ) (z : ℂ) (h_nonzero : f c ≠ 0) : deriv (fun (w : ℂ) => f (w + c) / f c) z = deriv f (z + c) / f c

theorem frac_cancel_const {x y c : ℂ} (hc : c ≠ 0) (hy : y ≠ 0) : x / c / (y / c) = x / y

theorem fc_log_deriv (c : ℂ) (f : ℂ → ℂ) (h_analytic : AnalyticOnNhd ℂ f (Metric.closedBall c 1)) (h_nonzero : f c ≠ 0) {z : ℂ} (hz_nonzero : f (z + c) ≠ 0) : deriv (fun (w : ℂ) => f (w + c) / f c) z / (f (z + c) / f c) = deriv f (z + c) / f (z + c)

theorem fc_bound (B : ℝ) (hB : B > 1) (R : ℝ) (hRpos : 0 < R) (hR : R < 1) (c : ℂ) (f : ℂ → ℂ) (h_nonzero : f c ≠ 0) (h_bound : ∀ z ∈ Metric.closedBall c R, ‖f z‖ ≤ B) (z : ℂ) : z ∈ Metric.closedBall 0 R → ‖(fun (w : ℂ) => f (w + c) / f c) z‖ ≤ B / ‖f c‖

theorem fc_zeros (r : ℝ) (h : r > 0) (c : ℂ) (f : ℂ → ℂ) (h_nonzero : f c ≠ 0) (h_analytic : AnalyticOnNhd ℂ f (Metric.closedBall c 1)) : (zerosetKfRc r 0 fun (z : ℂ) => f (z + c) / f c) = (fun (ρ : ℂ) => ρ - c) '' zerosetKfRc r c f

theorem analyticOrderAt_const_mul_eq (f : ℂ → ℂ) (a z0 : ℂ) (ha : a ≠ 0) : analyticOrderAt (fun (z : ℂ) => a * f z) z0 = analyticOrderAt f z0

theorem AnalyticAt.comp_add_const {f : ℂ → ℂ} {z0 c : ℂ} (hf : AnalyticAt ℂ f (z0 + c)) : AnalyticAt ℂ (fun (z : ℂ) => f (z + c)) z0

theorem AnalyticAt.of_comp_add_const {f : ℂ → ℂ} {z0 c : ℂ} (hg : AnalyticAt ℂ (fun (z : ℂ) => f (z + c)) z0) : AnalyticAt ℂ f (z0 + c)

theorem order_top_iff_comp_add (f : ℂ → ℂ) (z0 c : ℂ) : analyticOrderAt (fun (z : ℂ) => f (z + c)) z0 = ⊤ ↔ analyticOrderAt f (z0 + c) = ⊤

theorem enat_le_iff_forall_nat {x y : ℕ∞} : x ≤ y ↔ ∀ (n : ℕ), ↑n ≤ x → ↑n ≤ y

theorem natCast_le_order_const_mul_iff (f : ℂ → ℂ) (a z0 : ℂ) (ha : a ≠ 0) (n : ℕ) : ↑n ≤ analyticOrderAt (fun (z : ℂ) => a * f z) z0 ↔ ↑n ≤ analyticOrderAt f z0

theorem order_top_iff_const_mul (f : ℂ → ℂ) (a z0 : ℂ) (ha : a ≠ 0) : analyticOrderAt (fun (z : ℂ) => a * f z) z0 = ⊤ ↔ analyticOrderAt f z0 = ⊤

theorem analyticOrderAt_mul_const_eq (f : ℂ → ℂ) (a z0 : ℂ) (ha : a ≠ 0) : analyticOrderAt (fun (z : ℂ) => f z * a) z0 = analyticOrderAt f z0

theorem fc_m_order (r : ℝ) (h : r > 0) (c : ℂ) (f : ℂ → ℂ) (h_nonzero : f c ≠ 0) (h_analytic : AnalyticOnNhd ℂ f (Metric.closedBall c 1)) {ρ' : ℂ} (hρ' : ρ' ∈ zerosetKfRc r 0 fun (z : ℂ) => f (z + c) / f c) : analyticOrderAt (fun (z : ℂ) => f (z + c) / f c) ρ' = analyticOrderAt f (ρ' + c)

theorem DminusK (r1 R1 : ℝ) (hr1 : r1 > 0) (hR1 : R1 > 0) (c : ℂ) (f : ℂ → ℂ) (h_analytic : AnalyticOnNhd ℂ f (Metric.closedBall c 1)) (h_nonzero : f c ≠ 0) (z : ℂ) : (z ∈ Metric.closedBall 0 r1 \ zerosetKfRc R1 0 fun (w : ℂ) => f (w + c) / f c) ↔ z + c ∈ Metric.closedBall c r1 \ zerosetKfRc R1 c f

theorem shifted_zeros_correspondence (R1 : ℝ) (hR1 : R1 > 0) (c z : ℂ) (f : ℂ → ℂ) (h_nonzero : f c ≠ 0) (h_analytic : AnalyticOnNhd ℂ f (Metric.closedBall c 1)) (hfin_orig : (zerosetKfRc R1 c f).Finite) (hfin_shift : (zerosetKfRc R1 0 fun (u : ℂ) => f (u + c) / f c).Finite) : ∑ ρ ∈ hfin_orig.toFinset, ↑(analyticOrderAt f ρ).toNat / (z - ρ) = ∑ ρ' ∈ hfin_shift.toFinset, ↑(analyticOrderAt (fun (u : ℂ) => f (u + c) / f c) ρ').toNat / (z - c - ρ')

theorem final_ineq2 (B : ℝ) (hB : 1 < B) (r1 r R R1 : ℝ) (hr1pos : 0 < r1) (hr1_lt_r : r1 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR : R < 1) (c : ℂ) (f : ℂ → ℂ) (h_analytic : AnalyticOnNhd ℂ f (Metric.closedBall c 1)) (h_nonzero : f c ≠ 0) (h_bound : ∀ z ∈ Metric.closedBall c R, ‖f z‖ < B) (hfin : (zerosetKfRc R1 0 fun (z : ℂ) => f (z + c) / f c).Finite) (z : ℂ) : (z ∈ Metric.closedBall 0 r1 \ zerosetKfRc R1 0 fun (z : ℂ) => f (z + c) / f c) → ‖deriv (fun (z : ℂ) => f (z + c) / f c) z / (f (z + c) / f c) - ∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt (fun (w : ℂ) => f (w + c) / f c) ρ).toNat / (z - ρ)‖ ≤ (16 * r ^ 2 / (r - r1) ^ 3 + 1 / ((R ^ 2 / R1 - R1) * Real.log (R / R1))) * Real.log (B / ‖f c‖)

theorem log_Deriv_Expansion_Zeta (t : ℝ) (ht : |t| > 2) (r1 r R1 R : ℝ) (hr1_pos : 0 < r1) (hr1_lt_r : r1 < r) (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) : let c := 3 / 2 + I * ↑t; ∀ B > 1, (∀ z ∈ Metric.closedBall c R, ‖riemannZeta z‖ < B) → ∀ (hfin : (zerosetKfRc R1 c riemannZeta).Finite), ∀ z ∈ Metric.closedBall c r1 \ zerosetKfRc R1 c riemannZeta, ‖logDerivZeta z - ∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt riemannZeta ρ).toNat / (z - ρ)‖ ≤ (16 * r ^ 2 / (r - r1) ^ 3 + 1 / ((R ^ 2 / R1 - R1) * Real.log (R / R1))) * Real.log (B / ‖riemannZeta c‖)

theorem zeta32lower : ∃ a > 0, ∀ (t : ℝ), ‖riemannZeta (3 / 2 + I * ↑t)‖ ≥ a

theorem zeta32lower_log : ∃ A > 1, ∀ (t : ℝ), Real.log (1 / ‖riemannZeta (3 / 2 + I * ↑t)‖) ≤ A

theorem zeta32upper_pre : ∃ b > 1, ∀ (t : ℝ) (s : ℂ), ‖s‖ ≤ 1 → 2 < |t| → ‖riemannZeta (s + 3 / 2 + Complex.I * ↑t)‖ < b * |t|

theorem zeta32upper : ∃ b > 1, ∀ (t : ℝ), |t| > 2 → let c := 3 / 2 + I * ↑t; ∀ s ∈ Metric.closedBall c 1, ‖riemannZeta s‖ < b * |t|

theorem closedBall_subset_unit (c : ℂ) (R : ℝ) (hR_lt_1 : R < 1) : Metric.closedBall c R ⊆ Metric.closedBall c 1

theorem zeta_c_nonzero (t : ℝ) : riemannZeta (3 / 2 + I * ↑t) ≠ 0

theorem zeta_c_norm_pos (t : ℝ) : 0 < ‖riemannZeta (3 / 2 + I * ↑t)‖

theorem Zeta1_Zeta_Expand : ∃ A > 1, ∃ b > 1, ∀ (t : ℝ), |t| > 2 → ∀ (r1 r R1 R : ℝ), 0 < r1 → r1 < r → 0 < r → r < R1 → 0 < R1 → R1 < R → R < 1 → let c := 3 / 2 + I * ↑t; ∀ (hfin : (zerosetKfRc R1 c riemannZeta).Finite), ∀ z ∈ Metric.closedBall c r1 \ zerosetKfRc R1 c riemannZeta, ‖logDerivZeta z - ∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt riemannZeta ρ).toNat / (z - ρ)‖ ≤ (16 * r ^ 2 / (r - r1) ^ 3 + 1 / ((R ^ 2 / R1 - R1) * Real.log (R / R1))) * (Real.log |t| + Real.log b + A)

theorem helper_log_ratio_le_sum (b t x A : ℝ) (hb : b > 1) (ht : 0 < |t|) (hx : 0 < x) (hA : Real.log (1 / x) ≤ A) : Real.log (b * |t| / x) ≤ Real.log |t| + Real.log b + A

theorem helper_bound_sum_by_Klog (t b A : ℝ) (ht : |t| > 3) (hb : b > 1) (hA : A > 1) : ∃ K > 1, Real.log |t| + Real.log b + A ≤ K * Real.log (|t| + 2)

theorem Zeta1_Zeta_Expansion (r1 r : ℝ) (hr1_pos : 0 < r1) (hr1_lt_r : r1 < r) (hr_lt_R1 : r < 5 / 6) : ∃ C > 1, ∀ (t : ℝ), |t| > 3 → let c := 3 / 2 + I * ↑t; ∀ (hfin : (zerosetKfRc (5 / 6) c riemannZeta).Finite), ∀ z ∈ Metric.closedBall c r1 \ zerosetKfRc (5 / 6) c riemannZeta, ‖logDerivZeta z - ∑ ρ ∈ hfin.toFinset, ↑(analyticOrderAt riemannZeta ρ).toNat / (z - ρ)‖ ≤ C * (1 / (r - r1) ^ 3 + 1) * Real.log |t|