theorem div_cpow_eq_cpow_neg (a x s : ℂ) : a / x ^ s = a * x ^ (-s)

theorem one_div_cpow_eq_cpow_neg (x s : ℂ) : 1 / x ^ s = x ^ (-s)

theorem div_rpow_eq_rpow_neg (a x s : ℝ) (hx : 0 ≤ x) : a / x ^ s = a * x ^ (-s)

theorem div_rpow_neg_eq_rpow_div {x y s : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : x ^ (-s) / y ^ (-s) = (y / x) ^ s

theorem div_rpow_eq_rpow_div_neg {x y s : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : x ^ s / y ^ s = (y / x) ^ (-s)

def riemannzeta : Lean.ParserDescr

Equations

• riemannzeta = Lean.ParserDescr.node `riemannzeta 1024 (Lean.ParserDescr.symbol "ζ")

def derivriemannzeta : Lean.ParserDescr

Equations

• derivriemannzeta = Lean.ParserDescr.node `derivriemannzeta 1024 (Lean.ParserDescr.symbol "ζ'")

theorem ResidueOfTendsTo {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (hU : U ∈ nhds p) (hf : HolomorphicOn f (U \ {p})) {A : ℂ} (h_limit : Filter.Tendsto (fun (s : ℂ) => (s - p) * f s) (nhdsWithin p {p}ᶜ) (nhds A)) : ∃ V ∈ nhds p, BddAbove (norm ∘ (f - fun (s : ℂ) => A * (s - p)⁻¹) '' (V \ {p}))

theorem analyticAt_riemannZeta {s : ℂ} (s_ne_one : s ≠ 1) : AnalyticAt ℂ riemannZeta s

theorem differentiableAt_deriv_riemannZeta {s : ℂ} (s_ne_one : s ≠ 1) : DifferentiableAt ℂ (deriv riemannZeta) s

theorem riemannZetaResidue : ∃ U ∈ nhds 1, BddAbove (norm ∘ (riemannZeta - fun (s : ℂ) => (s - 1)⁻¹) '' (U \ {1}))

theorem deriv_eqOn_of_eqOn_punctured (f g : ℂ → ℂ) (U : Set ℂ) (p : ℂ) (hU_open : IsOpen U) (h_eq : Set.EqOn f g (U \ {p})) : Set.EqOn (deriv f) (deriv g) (U \ {p})

theorem analytic_deriv_bounded_near_point (f : ℂ → ℂ) {U : Set ℂ} {p : ℂ} (hU : IsOpen U) (hp : p ∈ U) (hf : HolomorphicOn f U) : deriv f =O[nhdsWithin p {p}ᶜ] 1

theorem map_inv_nhdsWithin_direct (h : ℂ → ℂ) (U : Set ℂ) (p A : ℂ) (A_ne_zero : A ≠ 0) : Filter.map h (nhdsWithin p U) ≤ nhds A → Filter.map (fun (x : ℂ) => (h x)⁻¹) (nhdsWithin p U) ≤ nhds A⁻¹

theorem map_inv_nhdsWithin_direct_alt (h : ℂ → ℂ) (p A : ℂ) (A_ne_zero : A ≠ 0) : Filter.map h (nhdsWithin p {p}ᶜ) ≤ nhds A → Filter.map (fun (x : ℂ) => (h x)⁻¹) (nhdsWithin p {p}ᶜ) ≤ nhds A⁻¹

theorem expression_eq_zero (A x p : ℂ) (h : x ≠ p) : A - A * x * (x - p)⁻¹ + A * p * (x - p)⁻¹ = 0

theorem field_identity (f f' x p : ℂ) (hf : f ≠ 0) (hp : x ≠ p) : f' * f⁻¹ + (x - p)⁻¹ = (f + f' * (x - p)) * ((x - p)⁻¹ * f⁻¹)

theorem derivative_const_plus_product {g : ℂ → ℂ} (A p x : ℂ) (hg : DifferentiableAt ℂ g x) : deriv ((fun (x : ℂ) => A) + g * fun (s : ℂ) => s - p) x = deriv g x * (x - p) + g x

theorem deriv_eq_of_eq (f g : ℂ → ℂ) (h : f = g) : deriv f = deriv g

theorem deriv_inv_complex : (deriv fun (z : ℂ) => z⁻¹) = fun (x : ℂ) => -(x ^ 2)⁻¹

theorem diff_translation (p : ℂ) : (deriv fun (x : ℂ) => x - p) = fun (x : ℂ) => 1

theorem deriv_inv_sub {x p : ℂ} (hp : x ≠ p) : deriv (fun (z : ℂ) => (z - p)⁻¹) x = -((x - p) ^ 2)⁻¹

theorem deriv_f_minus_A_inv_sub_clean (f : ℂ → ℂ) (A x p : ℂ) (hf : DifferentiableAt ℂ f x) (hp : x ≠ p) : deriv (f - fun (z : ℂ) => A * (z - p)⁻¹) x = deriv f x + A * ((x - p) ^ 2)⁻¹

theorem laurent_expansion_identity_alt (f f' A x p : ℂ) (h : x ≠ p) : (f' + A * ((x - p) ^ 2)⁻¹) * (x - p) + (f - A * (x - p)⁻¹) = f + f' * (x - p)

theorem nonZeroOfBddAbove {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (U_in_nhds : U ∈ nhds p) {A : ℂ} (A_ne_zero : A ≠ 0) (f_near_p : BddAbove (norm ∘ (f - fun (s : ℂ) => A * (s - p)⁻¹) '' (U \ {p}))) : ∃ V ∈ nhds p, IsOpen V ∧ ∀ s ∈ V \ {p}, f s ≠ 0

theorem logDerivResidue' {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (U_is_open : IsOpen U) (non_zero : ∀ x ∈ U \ {p}, f x ≠ 0) (holc : HolomorphicOn f (U \ {p})) (U_in_nhds : U ∈ nhds p) {A : ℂ} (A_ne_zero : A ≠ 0) (f_near_p : BddAbove (norm ∘ (f - fun (s : ℂ) => A * (s - p)⁻¹) '' (U \ {p}))) : (deriv f * f⁻¹ + fun (s : ℂ) => (s - p)⁻¹) =O[nhdsWithin p {p}ᶜ] 1

theorem logDerivResidue {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (non_zero : ∀ x ∈ U \ {p}, f x ≠ 0) (holc : HolomorphicOn f (U \ {p})) (U_in_nhds : U ∈ nhds p) {A : ℂ} (A_ne_zero : A ≠ 0) (f_near_p : BddAbove (norm ∘ (f - fun (s : ℂ) => A * (s - p)⁻¹) '' (U \ {p}))) : (deriv f * f⁻¹ + fun (s : ℂ) => (s - p)⁻¹) =O[nhdsWithin p {p}ᶜ] 1

theorem IsBigO_to_BddAbove {f : ℂ → ℂ} {p : ℂ} (f_near_p : f =O[nhdsWithin p {p}ᶜ] 1) : ∃ U ∈ nhds p, BddAbove (norm ∘ f '' (U \ {p}))

theorem BddAbove_to_IsBigO {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (hU : U ∈ nhds p) (bdd : BddAbove (norm ∘ f '' (U \ {p}))) : f =O[nhdsWithin p {p}ᶜ] 1

theorem logDerivResidue'' {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (non_zero : ∀ x ∈ U \ {p}, f x ≠ 0) (holc : HolomorphicOn f (U \ {p})) (U_in_nhds : U ∈ nhds p) {A : ℂ} (A_ne_zero : A ≠ 0) (f_near_p : BddAbove (norm ∘ (f - fun (s : ℂ) => A * (s - p)⁻¹) '' (U \ {p}))) : ∃ V ∈ nhds p, BddAbove (norm ∘ (deriv f * f⁻¹ + fun (s : ℂ) => (s - p)⁻¹) '' (V \ {p}))

theorem ResidueMult {f g : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (g_holc : HolomorphicOn g U) (U_in_nhds : U ∈ nhds p) {A : ℂ} (f_near_p : (f - fun (s : ℂ) => A * (s - p)⁻¹) =O[nhdsWithin p {p}ᶜ] 1) : (f * g - fun (s : ℂ) => A * g p * (s - p)⁻¹) =O[nhdsWithin p {p}ᶜ] 1

theorem riemannZetaLogDerivResidue : ∃ U ∈ nhds 1, BddAbove (norm ∘ (-(deriv riemannZeta / riemannZeta) - fun (s : ℂ) => (s - 1)⁻¹) '' (U \ {1}))

theorem riemannZetaLogDerivResidueBigO : (-deriv riemannZeta / riemannZeta - fun (z : ℂ) => (z - 1)⁻¹) =O[nhdsWithin 1 {1}ᶜ] 1

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

Equations

• riemannZeta0 N s = ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s + -↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)

def riemannzeta0 : Lean.ParserDescr

We use ζ to denote the Rieman zeta function and ζ₀ to denote the alternative Rieman zeta function..

Equations

• riemannzeta0 = Lean.ParserDescr.node `riemannzeta0 1024 (Lean.ParserDescr.symbol "ζ₀")

theorem riemannZeta0_apply (N : ℕ) (s : ℂ) : riemannZeta0 N s = ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s + (-↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)))

theorem Real.differentiableAt_cpow_const_of_ne (s : ℂ) {x : ℝ} (xpos : 0 < x) : DifferentiableAt ℝ (fun (x : ℝ) => ↑x ^ s) x

theorem Complex.one_div_cpow_eq {s : ℂ} {x : ℝ} (x_ne : x ≠ 0) : 1 / ↑x ^ s = ↑x ^ (-s)

theorem ContDiffOn.hasDeriv_deriv {φ : ℝ → ℂ} {s : Set ℝ} (φDiff : ContDiffOn ℝ 1 φ s) {x : ℝ} (x_in_s : s ∈ nhds x) : HasDerivAt φ (deriv φ x) x

theorem ContDiffOn.continuousOn_deriv {φ : ℝ → ℂ} {a b : ℝ} (φDiff : ContDiffOn ℝ 1 φ (Set.uIoo a b)) : ContinuousOn (deriv φ) (Set.uIoo a b)

theorem LinearDerivative_ofReal (x : ℝ) (a b : ℂ) : HasDerivAt (fun (t : ℝ) => a * ↑t + b) a x

theorem integral_deriv_mul_eq_sub' {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {a b : ℝ} {u v u' v' : ℝ → A} (hu : ∀ x ∈ Set.uIcc a b, HasDerivWithinAt u (u' x) (Set.uIcc a b) x) (hv : ∀ x ∈ Set.uIcc a b, HasDerivWithinAt v (v' x) (Set.uIcc a b) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) : ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

theorem sum_eq_int_deriv_aux2 {φ : ℝ → ℂ} {a b : ℝ} (c : ℂ) (φDiff : ∀ x ∈ Set.uIcc a b, HasDerivAt φ (deriv φ x) x) (derivφCont : ContinuousOn (deriv φ) (Set.uIcc a b)) : ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x

theorem sum_eq_int_deriv_aux_eq {φ : ℝ → ℂ} {a b : ℝ} {k : ℤ} (b_eq_kpOne : b = ↑k + 1) (φDiff : ∀ x ∈ Set.uIcc a b, HasDerivAt φ (deriv φ x) x) (derivφCont : ContinuousOn (deriv φ) (Set.uIcc a b)) : ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n = (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a - ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x

theorem sum_eq_int_deriv_aux_lt {φ : ℝ → ℂ} {a b : ℝ} {k : ℤ} (ha : a ∈ Set.Ico (↑k) b) (b_lt_kpOne : b < ↑k + 1) (φDiff : ∀ x ∈ Set.uIcc a b, HasDerivAt φ (deriv φ x) x) (derivφCont : ContinuousOn (deriv φ) (Set.uIcc a b)) : ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n = (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a - ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x

theorem sum_eq_int_deriv_aux1 {φ : ℝ → ℂ} {a b : ℝ} {k : ℤ} (ha : a ∈ Set.Ico (↑k) b) (b_le_kpOne : b ≤ ↑k + 1) (φDiff : ∀ x ∈ Set.uIcc a b, HasDerivAt φ (deriv φ x) x) (derivφCont : ContinuousOn (deriv φ) (Set.uIcc a b)) : ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n = (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a - ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x

theorem sum_eq_int_deriv_aux {φ : ℝ → ℂ} {a b : ℝ} {k : ℤ} (ha : a ∈ Set.Ico (↑k) b) (b_le_kpOne : b ≤ ↑k + 1) (φDiff : ∀ x ∈ Set.uIcc a b, HasDerivAt φ (deriv φ x) x) (derivφCont : ContinuousOn (deriv φ) (Set.uIcc a b)) : ∑ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋, φ ↑n = (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a - ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x

theorem interval_induction_aux_int (n : ℕ) (P : ℝ → ℝ → Prop) : (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) → (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) → ∀ (a b : ℝ), a < b → ↑n = ⌊b⌋ - ⌊a⌋ → P a b

theorem interval_induction (P : ℝ → ℝ → Prop) (base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) (step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b) (a b : ℝ) (hab : a < b) : P a b

theorem Finset.Ioc_diff_Ioc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} [DecidableEq α] (hb : b ∈ Icc a c) : Ioc a b = Ioc a c \ Ioc b c

** Partial summation ** (TODO : Add to Mathlib).

theorem Finset.sum_Ioc_add_sum_Ioc {a b c : ℤ} (f : ℤ → ℂ) (hb : b ∈ Icc a c) : ∑ n ∈ Ioc a b, f n + ∑ n ∈ Ioc b c, f n = ∑ n ∈ Ioc a c, f n

theorem integrability_aux₀ {a b : ℝ} : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.uIcc a b), ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1

theorem integrability_aux₁ {a b : ℝ} : IntervalIntegrable (fun (x : ℝ) => ↑⌊x⌋) MeasureTheory.volume a b

theorem integrability_aux₂ {a b : ℝ} : IntervalIntegrable (fun (x : ℝ) => 1 / 2 - ↑x) MeasureTheory.volume a b

theorem integrability_aux {a b : ℝ} : IntervalIntegrable (fun (x : ℝ) => ↑⌊x⌋ + 1 / 2 - ↑x) MeasureTheory.volume a b

theorem uIcc_subsets {a b c : ℝ} (hc : c ∈ Set.Icc a b) : Set.uIcc a c ⊆ Set.uIcc a b ∧ Set.uIcc c b ⊆ Set.uIcc a b

theorem sum_eq_int_deriv {φ : ℝ → ℂ} {a b : ℝ} (a_lt_b : a < b) (φDiff : ∀ x ∈ Set.uIcc a b, HasDerivAt φ (deriv φ x) x) (derivφCont : ContinuousOn (deriv φ) (Set.uIcc a b)) : ∑ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋, φ ↑n = (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a - ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x

theorem xpos_of_uIcc {a b : ℕ} (ha : a ∈ Set.Ioo 0 b) {x : ℝ} (x_in : x ∈ Set.uIcc ↑a ↑b) : 0 < x

theorem neg_s_ne_neg_one {s : ℂ} (s_ne_one : s ≠ 1) : -s ≠ -1

theorem ZetaSum_aux1₁ {a b : ℕ} {s : ℂ} (s_ne_one : s ≠ 1) (ha : a ∈ Set.Ioo 0 b) : ∫ (x : ℝ) in ↑a..↑b, 1 / ↑x ^ s = (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s)

theorem ZetaSum_aux1φDiff {s : ℂ} {x : ℝ} (xpos : 0 < x) : HasDerivAt (fun (t : ℝ) => 1 / ↑t ^ s) (deriv (fun (t : ℝ) => 1 / ↑t ^ s) x) x

theorem ZetaSum_aux1φderiv {s : ℂ} (s_ne_zero : s ≠ 0) {x : ℝ} (xpos : 0 < x) : deriv (fun (t : ℝ) => 1 / ↑t ^ s) x = (fun (x : ℝ) => -s * ↑x ^ (-(s + 1))) x

theorem ZetaSum_aux1derivφCont {s : ℂ} (s_ne_zero : s ≠ 0) {a b : ℕ} (ha : a ∈ Set.Ioo 0 b) : ContinuousOn (deriv fun (t : ℝ) => 1 / ↑t ^ s) (Set.uIcc ↑a ↑b)

theorem ZetaSum_aux1 {a b : ℕ} {s : ℂ} (s_ne_one : s ≠ 1) (s_ne_zero : s ≠ 0) (ha : a ∈ Set.Ioo 0 b) : ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s = (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) + s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))

theorem ZetaSum_aux1_1' {a b x : ℝ} (apos : 0 < a) (hx : x ∈ Set.Icc a b) : 0 < x

theorem ZetaSum_aux1_1 {a b x : ℝ} (apos : 0 < a) (a_lt_b : a < b) (hx : x ∈ Set.uIcc a b) : 0 < x

theorem ZetaSum_aux1_2 {a b c : ℝ} (apos : 0 < a) (a_lt_b : a < b) (h : c ≠ 0 ∧ 0 ∉ Set.uIcc a b) : ∫ (x : ℝ) in a..b, 1 / x ^ (c + 1) = (a ^ (-c) - b ^ (-c)) / c

theorem ZetaSum_aux1_3a (x : ℝ) : -(1 / 2) < ↑⌊x⌋ + 1 / 2 - x

theorem ZetaSum_aux1_3b (x : ℝ) : ↑⌊x⌋ + 1 / 2 - x ≤ 1 / 2

theorem ZetaSum_aux1_3 (x : ℝ) : ‖↑⌊x⌋ + 1 / 2 - x‖ ≤ 1 / 2

theorem ZetaSum_aux1_4' (x : ℝ) (hx : 0 < x) (s : ℂ) : ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ = ‖↑⌊x⌋ + 1 / 2 - x‖ / x ^ (s + 1).re

theorem ZetaSum_aux1_4 {a b : ℝ} (apos : 0 < a) (a_lt_b : a < b) {s : ℂ} : ∫ (x : ℝ) in a..b, ‖(↑⌊x⌋ + ↑1 / 2 - ↑x) / ↑x ^ (s + 1)‖ = ∫ (x : ℝ) in a..b, |↑⌊x⌋ + 1 / 2 - x| / x ^ (s + 1).re

theorem ZetaSum_aux1_5a {a b : ℝ} (apos : 0 < a) {s : ℂ} (x : ℝ) (h : x ∈ Set.Icc a b) : |↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1) ≤ 1 / x ^ (s.re + 1)

theorem ZetaSum_aux1_5b {a b : ℝ} (apos : 0 < a) (a_lt_b : a < b) {s : ℂ} (σpos : 0 < s.re) : IntervalIntegrable (fun (u : ℝ) => 1 / u ^ (s.re + 1)) MeasureTheory.volume a b

theorem measurable_floor_add_half_sub : Measurable fun (u : ℝ) => ↑⌊u⌋ + 1 / 2 - u

theorem ZetaSum_aux1_5c {a b : ℝ} {s : ℂ} : let g := fun (u : ℝ) => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1); MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict (Set.uIoc a b))

theorem ZetaSum_aux1_5d {a b : ℝ} (apos : 0 < a) (a_lt_b : a < b) {s : ℂ} (σpos : 0 < s.re) : IntervalIntegrable (fun (u : ℝ) => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)) MeasureTheory.volume a b

theorem ZetaSum_aux1_5 {a b : ℝ} (apos : 0 < a) (a_lt_b : a < b) {s : ℂ} (σpos : 0 < s.re) : ∫ (x : ℝ) in a..b, |↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1) ≤ ∫ (x : ℝ) in a..b, 1 / x ^ (s.re + 1)

theorem ZetaBnd_aux1a {a b : ℝ} (apos : 0 < a) (a_lt_b : a < b) {s : ℂ} (σpos : 0 < s.re) : ∫ (x : ℝ) in a..b, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤ (a ^ (-s.re) - b ^ (-s.re)) / s.re

theorem tsum_eq_partial_add_tail {N : ℕ} (f : ℕ → ℂ) (hf : Summable f) : ∑' (n : ℕ), f n = ∑ n ∈ Finset.range N, f n + ∑' (n : ℕ), f (n + N)

theorem Finset.Ioc_eq_Ico (M N : ℕ) : Ioc N M = Ico (N + 1) (M + 1)

theorem Finset.Ioc_eq_Icc (M N : ℕ) : Ioc N M = Icc (N + 1) M

theorem Finset.Icc_eq_Ico (M N : ℕ) : Icc N M = Ico N (M + 1)

theorem finsetSum_tendsto_tsum {N : ℕ} {f : ℕ → ℂ} (hf : Summable f) : Filter.Tendsto (fun (k : ℕ) => ∑ n ∈ Finset.Ico N k, f n) Filter.atTop (nhds (∑' (n : ℕ), f (n + N)))

theorem tendsto_coe_atTop : Filter.Tendsto (fun (n : ℕ) => ↑n) Filter.atTop Filter.atTop

theorem Summable_rpow {s : ℂ} (s_re_gt : 1 < s.re) : Summable fun (n : ℕ) => 1 / ↑n ^ s

theorem Finset_coe_Nat_Int (f : ℤ → ℂ) (m n : ℕ) : ∑ x ∈ Finset.Ioc m n, f ↑x = ∑ x ∈ Finset.Ioc ↑m ↑n, f x

theorem Complex.cpow_tendsto {s : ℂ} (s_re_gt : 1 < s.re) : Filter.Tendsto (fun (x : ℕ) => ↑x ^ (1 - s)) Filter.atTop (nhds 0)

theorem Complex.cpow_inv_tendsto {s : ℂ} (hs : 0 < s.re) : Filter.Tendsto (fun (x : ℕ) => (↑x ^ s)⁻¹) Filter.atTop (nhds 0)

theorem ZetaSum_aux2a : ∃ (C : ℝ), ∀ (x : ℝ), ‖↑⌊x⌋ + 1 / 2 - x‖ ≤ C

theorem ZetaSum_aux3 {N : ℕ} {s : ℂ} (s_re_gt : 1 < s.re) : Filter.Tendsto (fun (k : ℕ) => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) Filter.atTop (nhds (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))

theorem integrableOn_of_Zeta0_fun {N : ℕ} (N_pos : 0 < N) {s : ℂ} (s_re_gt : 0 < s.re) : MeasureTheory.IntegrableOn (fun (x : ℝ) => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) (Set.Ioi ↑N) MeasureTheory.volume

theorem ZetaSum_aux2 {N : ℕ} (N_pos : 0 < N) {s : ℂ} (s_re_gt : 1 < s.re) : ∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s = -↑N ^ (1 - s) / (1 - s) - ↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))

theorem ZetaBnd_aux1b (N : ℕ) (Npos : 1 ≤ N) {σ t : ℝ} (σpos : 0 < σ) : ‖∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * Complex.I + 1)‖ ≤ ↑N ^ (-σ) / σ

theorem ZetaBnd_aux1 (N : ℕ) (Npos : 1 ≤ N) {σ t : ℝ} (hσ : σ ∈ Set.Ioc 0 2) (ht : 2 ≤ |t|) : ‖(↑σ + ↑t * Complex.I) * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * Complex.I + 1)‖ ≤ 2 * |t| * ↑N ^ (-σ) / σ

theorem ZetaBnd_aux1p (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (hσ : σ ∈ Set.Ioc 0 2) : (fun (t : ℝ) => ‖(↑σ + ↑t * Complex.I) * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * Complex.I + 1)‖) =O[Filter.principal {t : ℝ | 2 ≤ |t|}] fun (t : ℝ) => |t| * ↑N ^ (-σ) / σ

theorem isOpen_aux : IsOpen {z : ℂ | z ≠ 1 ∧ 0 < z.re}

theorem integrable_log_over_pow {r : ℝ} (rneg : r < 0) {N : ℕ} (Npos : 0 < N) : MeasureTheory.IntegrableOn (fun (x : ℝ) => ‖x ^ (r - 1)‖ * ‖Real.log x‖) (Set.Ioi ↑N) MeasureTheory.volume

theorem integrableOn_of_Zeta0_fun_log {N : ℕ} (Npos : 0 < N) {s : ℂ} (s_re_gt : 0 < s.re) : MeasureTheory.IntegrableOn (fun (x : ℝ) => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) * -↑(Real.log x)) (Set.Ioi ↑N) MeasureTheory.volume

theorem hasDerivAt_Zeta0Integral {N : ℕ} (Npos : 0 < N) {s : ℂ} (hs : s ∈ {s : ℂ | 0 < s.re}) : HasDerivAt (fun (z : ℂ) => ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1)) (∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑(Real.log x)) s

noncomputable def ζ₀' (N : ℕ) (s : ℂ) : ℂ

Equations

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

theorem HasDerivAt_neg_cpow_over2 {N : ℕ} (Npos : 0 < N) (s : ℂ) : HasDerivAt (fun (x : ℂ) => -↑N ^ (-x) / 2) (-(-↑(Real.log ↑N) * ↑N ^ (-s)) / 2) s

theorem HasDerivAt_cpow_over_var (N : ℕ) {z : ℂ} (z_ne_zero : z ≠ 0) : HasDerivAt (fun (z : ℂ) => -↑N ^ z / z) (↑N ^ z / z ^ 2 - ↑(Real.log ↑N) * ↑N ^ z / z) z

theorem HasDerivAtZeta0 {N : ℕ} (Npos : 0 < N) {s : ℂ} (reS_pos : 0 < s.re) (s_ne_one : s ≠ 1) : HasDerivAt (riemannZeta0 N) (ζ₀' N s) s

theorem HolomorphicOn_riemannZeta0 {N : ℕ} (N_pos : 0 < N) : HolomorphicOn (riemannZeta0 N) {s : ℂ | s ≠ 1 ∧ 0 < s.re}

theorem HolomophicOn_riemannZeta : HolomorphicOn riemannZeta {s : ℂ | s ≠ 1}

theorem isPathConnected_aux : IsPathConnected {z : ℂ | z ≠ 1 ∧ 0 < z.re}

theorem Zeta0EqZeta {N : ℕ} (N_pos : 0 < N) {s : ℂ} (reS_pos : 0 < s.re) (s_ne_one : s ≠ 1) : riemannZeta0 N s = riemannZeta s

theorem DerivZeta0EqDerivZeta {N : ℕ} (N_pos : 0 < N) {s : ℂ} (reS_pos : 0 < s.re) (s_ne_one : s ≠ 1) : deriv (riemannZeta0 N) s = deriv riemannZeta s

theorem le_trans₄ {α : Type u_1} [Preorder α] {a b c d : α} : a ≤ b → b ≤ c → c ≤ d → a ≤ d

theorem lt_trans₄ {α : Type u_1} [Preorder α] {a b c d : α} : a < b → b < c → c < d → a < d

theorem norm_add₄_le {E : Type u_1} [SeminormedAddGroup E] (a b c d : E) : ‖a + b + c + d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖

theorem norm_add₅_le {E : Type u_1} [SeminormedAddGroup E] (a b c d e : E) : ‖a + b + c + d + e‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖ + ‖e‖

theorem norm_add₆_le {E : Type u_1} [SeminormedAddGroup E] (a b c d e f : E) : ‖a + b + c + d + e + f‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖ + ‖e‖ + ‖f‖

theorem add_le_add_le_add {α : Type u_1} [Add α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a b c d e f : α} (h₁ : a ≤ b) (h₂ : c ≤ d) (h₃ : e ≤ f) : a + c + e ≤ b + d + f

theorem add_le_add_le_add_le_add {α : Type u_1} [Add α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a b c d e f g h : α} (h₁ : a ≤ b) (h₂ : c ≤ d) (h₃ : e ≤ f) (h₄ : g ≤ h) : a + c + e + g ≤ b + d + f + h

theorem mul_le_mul₃ {α : Type u_1} {a b c d e f : α} [MulZeroClass α] [Preorder α] [PosMulMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c ≤ d) (h₃ : e ≤ f) (c0 : 0 ≤ c) (b0 : 0 ≤ b) (e0 : 0 ≤ e) : a * c * e ≤ b * d * f

theorem ZetaBnd_aux2 {n : ℕ} {t A σ : ℝ} (Apos : 0 < A) (σpos : 0 < σ) (n_le_t : ↑n ≤ |t|) (σ_ge : 1 - A / Real.log |t| ≤ σ) : ‖↑n ^ (-(↑σ + ↑t * Complex.I))‖ ≤ (↑n)⁻¹ * Real.exp A

theorem logt_gt_one {t : ℝ} (t_ge : 3 < |t|) : 1 < Real.log |t|

theorem UpperBnd_aux {A σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (t_gt : 3 < |t|) (σ_ge : 1 - A / Real.log |t| ≤ σ) : let N := ⌊|t|⌋₊; 0 < N ∧ ↑N ≤ |t| ∧ 1 < Real.log |t| ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * Complex.I ≠ 1

theorem UpperBnd_aux2 {A σ t : ℝ} (t_ge : 3 < |t|) (σ_ge : 1 - A / Real.log |t| ≤ σ) : |t| ^ (1 - σ) ≤ Real.exp A

theorem riemannZeta0_zero_aux (N : ℕ) (Npos : 0 < N) : ∑ x ∈ Finset.Ico 0 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹

theorem UpperBnd_aux3 {A C σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (σ_ge : 1 - A / Real.log |t| ≤ σ) (t_gt : 3 < |t|) (hC : 2 ≤ C) : let N := ⌊|t|⌋₊; ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * Complex.I))‖ ≤ Real.exp A * C * Real.log |t|

theorem Nat.self_div_floor_bound {t : ℝ} (t_ge : 1 ≤ |t|) : let N := ⌊|t|⌋₊; |t| / ↑N ∈ Set.Icc 1 2

theorem UpperBnd_aux5 {σ t : ℝ} (t_ge : 3 < |t|) (σ_le : σ ≤ 2) : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4

theorem UpperBnd_aux6 {σ t : ℝ} (t_ge : 3 < |t|) (hσ : σ ∈ Set.Ioc (1 / 2) 2) (neOne : ↑σ + ↑t * Complex.I ≠ 1) (Npos : 0 < ⌊|t|⌋₊) (N_le_t : ↑⌊|t|⌋₊ ≤ |t|) : ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * Complex.I)‖ ≤ |t| ^ (1 - σ) * 2 ∧ ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ) ∧ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)

theorem ZetaUpperBnd' {A σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) : let C := Real.exp A * (5 + 8 * 2); let N := ⌊|t|⌋₊; let s := ↑σ + ↑t * Complex.I; ‖∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s‖ + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ + ‖s * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤ C * Real.log |t|

theorem ZetaUpperBnd : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Icc (1 - A / Real.log |t|) 2 → ‖riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * Real.log |t|

theorem norm_complex_log_ofNat (n : ℕ) : ‖Complex.log ↑n‖ = Real.log ↑n

theorem Real.log_natCast_monotone : Monotone fun (n : ℕ) => log ↑n

theorem Finset.Icc0_eq (N : ℕ) : Icc 0 N = {0} ∪ Icc 1 N

theorem harmonic_eq_sum_Icc0_aux (N : ℕ) : ∑ i ∈ Finset.Icc 0 N, (↑i)⁻¹ = ∑ i ∈ Finset.Icc 1 N, (↑i)⁻¹

theorem harmonic_eq_sum_Icc0 (N : ℕ) : ∑ i ∈ Finset.Icc 0 N, (↑i)⁻¹ = ↑(harmonic N)

theorem DerivUpperBnd_aux1 {A C σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (σ_ge : 1 - A / Real.log |t| ≤ σ) (t_gt : 3 < |t|) (hC : 2 ≤ C) : let N := ⌊|t|⌋₊; ‖∑ n ∈ Finset.range (N + 1), -1 / ↑n ^ (↑σ + ↑t * Complex.I) * ↑(Real.log ↑n)‖ ≤ Real.exp A * C * Real.log |t| ^ 2

theorem DerivUpperBnd_aux2 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) : let N := ⌊|t|⌋₊; let s := ↑σ + ↑t * Complex.I; 0 < N → ↑N ≤ |t| → s ≠ 1 → 1 / 2 < σ → ‖-↑N ^ (1 - s) / (1 - s) ^ 2‖ ≤ Real.exp A * 2 * (1 / 3)

theorem DerivUpperBnd_aux3 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) : let N := ⌊|t|⌋₊; let s := ↑σ + ↑t * Complex.I; 0 < N → ↑N ≤ |t| → s ≠ 1 → 1 / 2 < σ → ‖↑(Real.log ↑N) * ↑N ^ (1 - s) / (1 - s)‖ ≤ Real.exp A * 2 * Real.log |t|

theorem DerivUpperBnd_aux4 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) : let N := ⌊|t|⌋₊; let s := ↑σ + ↑t * Complex.I; 0 < N → ↑N ≤ |t| → s ≠ 1 → 1 / 2 < σ → ‖↑(Real.log ↑N) * ↑N ^ (-s) / 2‖ ≤ Real.exp A * Real.log |t|

theorem DerivUpperBnd_aux5 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) : let N := ⌊|t|⌋₊; let s := ↑σ + ↑t * Complex.I; 0 < N → 1 / 2 < σ → ‖1 * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)‖ ≤ 1 / 3 * (2 * |t| * ↑N ^ (-σ) / σ)

theorem DerivUpperBnd_aux6 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) : let N := ⌊|t|⌋₊; 0 < N → ↑N ≤ |t| → ↑σ + ↑t * Complex.I ≠ 1 → 1 / 2 < σ → 2 * |t| * ↑N ^ (-σ) / σ ≤ 2 * (8 * Real.exp A)

theorem DerivUpperBnd_aux7_1 {x σ t : ℝ} (hx : 1 ≤ x) : let s := ↑σ + ↑t * Complex.I; ‖(↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑(Real.log x)‖ = |↑⌊x⌋ + 1 / 2 - x| * x ^ (-σ - 1) * Real.log x

theorem DerivUpperBnd_aux7_2 {x σ : ℝ} (hx : 1 ≤ x) : |↑⌊x⌋ + 1 / 2 - x| * x ^ (-σ - 1) * Real.log x ≤ x ^ (-σ - 1) * Real.log x

theorem DerivUpperBnd_aux7_3 {x σ : ℝ} (xpos : 0 < x) (σnz : σ ≠ 0) : HasDerivAt (fun (t : ℝ) => -(1 / σ ^ 2 * t ^ (-σ) + 1 / σ * t ^ (-σ) * Real.log t)) (x ^ (-σ - 1) * Real.log x) x

theorem DerivUpperBnd_aux7_3' {a σ : ℝ} (apos : 0 < a) (σnz : σ ≠ 0) (x : ℝ) : x ∈ Set.Ici a → HasDerivAt (fun (t : ℝ) => -(1 / σ ^ 2 * t ^ (-σ) + 1 / σ * t ^ (-σ) * Real.log t)) (x ^ (-σ - 1) * Real.log x) x

theorem DerivUpperBnd_aux7_nonneg {a σ : ℝ} (ha : 1 ≤ a) (x : ℝ) : x ∈ Set.Ioi a → 0 ≤ x ^ (-σ - 1) * Real.log x

theorem DerivUpperBnd_aux7_tendsto {σ : ℝ} (σpos : 0 < σ) : Filter.Tendsto (fun (t : ℝ) => -(1 / σ ^ 2 * t ^ (-σ) + 1 / σ * t ^ (-σ) * Real.log t)) Filter.atTop (nhds 0)

theorem DerivUpperBnd_aux7_4 {a σ : ℝ} (σpos : 0 < σ) (ha : 1 ≤ a) : MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ (-σ - 1) * Real.log x) (Set.Ioi a) MeasureTheory.volume

theorem DerivUpperBnd_aux7_5 {a σ : ℝ} (σpos : 0 < σ) (ha : 1 ≤ a) : MeasureTheory.IntegrableOn (fun (x : ℝ) => |↑⌊x⌋ + 1 / 2 - x| * x ^ (-σ - 1) * Real.log x) (Set.Ioi a) MeasureTheory.volume

theorem DerivUpperBnd_aux7_integral_eq {a σ : ℝ} (ha : 1 ≤ a) (σpos : 0 < σ) : ∫ (x : ℝ) in Set.Ioi a, x ^ (-σ - 1) * Real.log x = 1 / σ ^ 2 * a ^ (-σ) + 1 / σ * a ^ (-σ) * Real.log a

theorem DerivUpperBnd_aux7 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) : let N := ⌊|t|⌋₊; let s := ↑σ + ↑t * Complex.I; 0 < N → ↑N ≤ |t| → s ≠ 1 → 1 / 2 < σ → ‖s * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑(Real.log x)‖ ≤ 6 * |t| * ↑N ^ (-σ) / σ * Real.log |t|

theorem ZetaDerivUpperBnd' {A σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (t_gt : 3 < |t|) (hσ : σ ∈ Set.Icc (1 - A / Real.log |t|) 2) : let C := Real.exp A * 59; let N := ⌊|t|⌋₊; let s := ↑σ + ↑t * Complex.I; ‖∑ n ∈ Finset.range (N + 1), -1 / ↑n ^ s * ↑(Real.log ↑n)‖ + ‖-↑N ^ (1 - s) / (1 - s) ^ 2‖ + ‖↑(Real.log ↑N) * ↑N ^ (1 - s) / (1 - s)‖ + ‖↑(Real.log ↑N) * ↑N ^ (-s) / 2‖ + ‖1 * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)‖ + ‖s * ∫ (x : ℝ) in Set.Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑(Real.log x)‖ ≤ C * Real.log |t| ^ 2

theorem ZetaDerivUpperBnd : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Icc (1 - A / Real.log |t|) 2 → ‖deriv riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * Real.log |t| ^ 2

theorem Tendsto_nhdsWithin_punctured_map_add {f : ℝ → ℝ} (a x : ℝ) (f_mono : StrictMono f) (f_iso : Isometry f) : Filter.Tendsto (fun (y : ℝ) => f y + a) (nhdsWithin x (Set.Ioi x)) (nhdsWithin (f x + a) (Set.Ioi (f x + a)))

theorem Tendsto_nhdsWithin_punctured_add (a x : ℝ) : Filter.Tendsto (fun (y : ℝ) => y + a) (nhdsWithin x (Set.Ioi x)) (nhdsWithin (x + a) (Set.Ioi (x + a)))

theorem riemannZeta_isBigO_near_one_horizontal : (fun (x : ℝ) => riemannZeta (1 + ↑x)) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => 1 / ↑x

theorem ZetaNear1BndFilter : (fun (σ : ℝ) => riemannZeta ↑σ) =O[nhdsWithin 1 (Set.Ioi 1)] fun (σ : ℝ) => 1 / (↑σ - 1)

theorem ZetaNear1BndExact : ∃ (c : ℝ) (_ : 0 < c), ∀ σ ∈ Set.Ioc 1 2, ‖riemannZeta ↑σ‖ ≤ c / (σ - 1)

theorem norm_zeta_product_ge_one {x : ℝ} (hx : 0 < x) (y : ℝ) : ‖riemannZeta (1 + ↑x) ^ 3 * riemannZeta (1 + ↑x + Complex.I * ↑y) ^ 4 * riemannZeta (1 + ↑x + 2 * Complex.I * ↑y)‖ ≥ 1

For positive x and nonzero y we have that $|\zeta(x)^3 \cdot \zeta(x+iy)^4 \cdot \zeta(x+2iy)| \ge 1$.

theorem ZetaLowerBound1_aux1 {σ t : ℝ} (this : 1 ≤ ‖riemannZeta ↑σ‖ ^ 3 * ‖riemannZeta (↑σ + Complex.I * ↑t)‖ ^ 4 * ‖riemannZeta (↑σ + 2 * Complex.I * ↑t)‖) : ‖riemannZeta ↑σ‖ ^ (3 / 4) * ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4) * ‖riemannZeta (↑σ + ↑t * Complex.I)‖ ≥ 1

theorem ZetaLowerBound1 {σ t : ℝ} (σ_gt : 1 < σ) : ‖riemannZeta ↑σ‖ ^ (3 / 4) * ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4) * ‖riemannZeta (↑σ + ↑t * Complex.I)‖ ≥ 1

theorem ZetaLowerBound2 {σ t : ℝ} (σ_gt : 1 < σ) : 1 / (‖riemannZeta ↑σ‖ ^ (3 / 4) * ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4)) ≤ ‖riemannZeta (↑σ + ↑t * Complex.I)‖

theorem ZetaLowerBound3_aux1 (A : ℝ) (ha : A ∈ Set.Ioc 0 (1 / 2)) (t : ℝ) (ht_2 : 3 < |2 * t|) : 0 < A / Real.log |2 * t|

theorem ZetaLowerBound3_aux2 {C σ t : ℝ} (ζ_2t_bound : ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ≤ C * Real.log |2 * t|) : ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4) ≤ (C * Real.log |2 * t|) ^ (1 / 4)

theorem ZetaLowerBound3_aux3 {A : ℝ} : 0 < A → ∀ {C : ℝ}, 0 < C → ∀ {c_near : ℝ}, 0 < c_near → ∀ (σ t : ℝ), 3 < |t| → ∀ (σ_gt : 1 < σ), c_near ^ (3 / 4) * ((-1 + σ) ^ (3 / 4))⁻¹ * C ^ (1 / 4) * Real.log |t * 2| ^ (1 / 4) = c_near ^ (3 / 4) * C ^ (1 / 4) * Real.log |t * 2| ^ (1 / 4) * (-1 + σ) ^ (-3 / 4)

theorem ZetaLowerBound3_aux4 (A : ℝ) : A ∈ Set.Ioc 0 (1 / 2) → ∀ (C : ℝ) (hC : 0 < C) (c_near : ℝ) (hc_near : 0 < c_near) {σ : ℝ} (t : ℝ) (ht : 3 < |t|) (σ_gt : 1 < σ), 0 < c_near ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * C ^ (1 / 4) * Real.log |2 * t| ^ (1 / 4)

theorem ZetaLowerBound3_aux5 {σ : ℝ} (t : ℝ) (this : ‖riemannZeta ↑σ‖ ^ (3 / 4) * ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4) * ‖riemannZeta (↑σ + ↑t * Complex.I)‖ ≥ 1) : 0 < ‖riemannZeta ↑σ‖ ^ (3 / 4) * ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4)

theorem ZetaLowerBound3 : ∃ c > 0, ∀ {σ : ℝ}, σ ∈ Set.Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → c * (σ - 1) ^ (3 / 4) / Real.log |t| ^ (1 / 4) ≤ ‖riemannZeta (↑σ + ↑t * Complex.I)‖

theorem ZetaInvBound1 {σ t : ℝ} (σ_gt : 1 < σ) : 1 / ‖riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ ‖riemannZeta ↑σ‖ ^ (3 / 4) * ‖riemannZeta (↑σ + 2 * ↑t * Complex.I)‖ ^ (1 / 4)

theorem Ioi_union_Iio_mem_cocompact {a : ℝ} (ha : 0 ≤ a) : Set.Ioi a ∪ Set.Iio (-a) ∈ Filter.cocompact ℝ

theorem lt_abs_mem_cocompact {a : ℝ} (ha : 0 ≤ a) : {t : ℝ | a < |t|} ∈ Filter.cocompact ℝ

theorem ZetaInvBound2 : ∃ C > 0, ∀ {σ : ℝ}, σ ∈ Set.Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * (σ - 1) ^ (-3 / 4) * Real.log |t| ^ (1 / 4)

theorem deriv_fun_re {t : ℝ} {f : ℂ → ℂ} (diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * Complex.I)) : (deriv fun {σ₂ : ℝ} => f (↑σ₂ + ↑t * Complex.I)) = fun (σ : ℝ) => deriv f (↑σ + ↑t * Complex.I)

theorem Zeta_eq_int_derivZeta {σ₁ σ₂ t : ℝ} (t_ne_zero : t ≠ 0) : ∫ (σ : ℝ) in σ₁..σ₂, deriv riemannZeta (↑σ + ↑t * Complex.I) = riemannZeta (↑σ₂ + ↑t * Complex.I) - riemannZeta (↑σ₁ + ↑t * Complex.I)

theorem Zeta_diff_Bnd : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ₁ σ₂ t : ℝ), 3 < |t| → 1 - A / Real.log |t| ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖riemannZeta (↑σ₂ + ↑t * Complex.I) - riemannZeta (↑σ₁ + ↑t * Complex.I)‖ ≤ C * Real.log |t| ^ 2 * (σ₂ - σ₁)

theorem ZetaInvBnd_aux' {t : ℝ} (logt_gt_one : 1 < Real.log |t|) : Real.log |t| < Real.log |t| ^ 9

theorem ZetaInvBnd_aux {t : ℝ} (logt_gt_one : 1 < Real.log |t|) : Real.log |t| ≤ Real.log |t| ^ 9

theorem ZetaInvBnd_aux2 {A C₁ C₂ : ℝ} (Apos : 0 < A) (C₁pos : 0 < C₁) (C₂pos : 0 < C₂) (hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4) : 0 < (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹

theorem ZetaInvBnd : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Ico (1 - A / Real.log |t| ^ 9) 1 → 1 / ‖riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * Real.log |t| ^ 7

theorem ZetaInvBnd' : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Ico (1 - A / Real.log |t| ^ 9) (1 + A / Real.log |t| ^ 9) → 1 / ‖riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * Real.log |t| ^ 7

theorem ZetaLowerBnd : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)) (c : ℝ) (_ : 0 < c), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Ico (1 - A / Real.log |t| ^ 9) 1 → c / Real.log |t| ^ 7 ≤ ‖riemannZeta (↑σ + ↑t * Complex.I)‖

theorem ZetaZeroFree : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Ico (1 - A / Real.log |t| ^ 9) 1 → riemannZeta (↑σ + ↑t * Complex.I) ≠ 0

theorem LogDerivZetaBnd : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Ico (1 - A / Real.log |t| ^ 9) 1 → ‖deriv riemannZeta (↑σ + ↑t * Complex.I) / riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * Real.log |t| ^ 9

theorem LogDerivZetaBnd' : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Ico (1 - A / Real.log |t| ^ 9) (1 + A / Real.log |t| ^ 9) → ‖deriv riemannZeta (↑σ + ↑t * Complex.I) / riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * Real.log |t| ^ 9

theorem LogDerivZetaBndUniform : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ T t : ℝ), 3 < |t| → |t| ≤ T → σ ∈ Set.Ico (1 - A / Real.log T ^ 9) 1 → ‖deriv riemannZeta (↑σ + ↑t * Complex.I) / riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * Real.log T ^ 9

theorem LogDerivZetaBndUniform' : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (σ T t : ℝ), 3 < |t| → |t| ≤ T → σ ∈ Set.Ico (1 - A / Real.log T ^ 9) (1 + A / Real.log T ^ 9) → ‖deriv riemannZeta (↑σ + ↑t * Complex.I) / riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * Real.log T ^ 9

theorem ZetaNoZerosOn1Line (t : ℝ) : riemannZeta (1 + ↑t * Complex.I) ≠ 0

theorem ZetaCont : ContinuousOn riemannZeta (Set.univ \ {1})

theorem ZetaNoZerosInBox (T : ℝ) : ∃ (σ : ℝ) (_ : σ < 1), ∀ (t : ℝ), |t| ≤ T → ∀ σ' ≥ σ, riemannZeta (↑σ' + ↑t * Complex.I) ≠ 0

theorem LogDerivZetaHoloOn {S : Set ℂ} (s_ne_one : 1 ∉ S) (nonzero : ∀ s ∈ S, riemannZeta s ≠ 0) : HolomorphicOn (fun (s : ℂ) => deriv riemannZeta s / riemannZeta s) S

theorem LogDerivZetaHolcSmallT : ∃ (σ₂ : ℝ) (_ : σ₂ < 1), HolomorphicOn (fun (s : ℂ) => deriv riemannZeta s / riemannZeta s) (Set.uIcc σ₂ 2 ×ℂ Set.uIcc (-3) 3 \ {1})

theorem LogDerivZetaHolcLargeT : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)), ∀ (T : ℝ), 3 ≤ T → HolomorphicOn (fun (s : ℂ) => deriv riemannZeta s / riemannZeta s) (Set.Icc (1 - A / Real.log T ^ 9) 2 ×ℂ Set.Icc (-T) T \ {1})

theorem LogDerivZetaBndAlt : ∃ A > 0, ∀ σ ∈ Set.Ico (1 / 2) 1, (fun (t : ℝ) => deriv riemannZeta (↑σ + ↑t * Complex.I) / riemannZeta (↑σ + ↑t * Complex.I)) =O[Filter.cocompact ℝ ⊓ Filter.principal {t : ℝ | 1 - A / Real.log |t| ^ 9 < σ}] fun (t : ℝ) => Real.log |t| ^ 9