From 7293a4caf263ced47767d65afe7baa8c4a5bddfc Mon Sep 17 00:00:00 2001 From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com> Date: Tue, 30 Apr 2024 11:05:58 -0400 Subject: [PATCH 1/7] ZetaBnd_aux1b work --- PrimeNumberTheoremAnd/ZetaBounds.lean | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/PrimeNumberTheoremAnd/ZetaBounds.lean b/PrimeNumberTheoremAnd/ZetaBounds.lean index a5b95e01..20d8a329 100644 --- a/PrimeNumberTheoremAnd/ZetaBounds.lean +++ b/PrimeNumberTheoremAnd/ZetaBounds.lean @@ -721,17 +721,21 @@ def C_aux1 := 200 -- two times C_aux1' \begin{lemma}[ZetaBnd_aux1b]\label{ZetaBnd_aux1b}\lean{ZetaBnd_aux1b}\leanok For any $N\ge1$ and $s\in \C$, $\sigma=\Re(s)\in(0,2]$, $$ -\left| s\int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx \right| -\ll |t| \frac{N^{-\sigma}}{\sigma}, +\left| \int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx \right| +\ll \frac{N^{-\sigma}}{\sigma}, $$ -as $|t|\to\infty$. +with an absolute implied constant. \end{lemma} %%-/ -lemma ZetaBnd_aux1b (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (σpos : 0 < σ) : - ∀ (t : ℝ) (ht : ct_aux1 < |t|), +lemma ZetaBnd_aux1b (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (σpos : 0 < σ) {t : ℝ} (ht : ct_aux1 < |t|) : ‖∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ ((σ + t * I) + 1)‖ ≤ C_aux1' * N ^ (-σ) / σ := by - have := @ZetaSum_aux1a (a := N) + have := @ZetaSum_aux1a (a := N) ?_ (by positivity) sorry ?_ sorry + have := @tendsto_nhds_unique (X := ℂ) (Y := ℕ) (l := atTop) + (f := fun k ↦ ((k : ℂ) ^ (1 - s) - (N : ℂ) ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑k ^ s) - 1 / 2 * (1 / ↑N ^ s) + + s * ∫ (x : ℝ) in (N : ℝ)..k, (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1))) + (b := (- N ^ (1 - s)) / (1 - s) - N ^ (-s) / 2 + + s * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1))) sorry /-%% \begin{proof}\uses{ZetaSum_aux1a} From fd9c70923d27261024dd2018e8309a30134b33fd Mon Sep 17 00:00:00 2001 From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com> Date: Tue, 30 Apr 2024 11:25:18 -0400 Subject: [PATCH 2/7] ZetaBnd_aux1 golf --- PrimeNumberTheoremAnd/ZetaBounds.lean | 38 +++++++++++++-------------- 1 file changed, 18 insertions(+), 20 deletions(-) diff --git a/PrimeNumberTheoremAnd/ZetaBounds.lean b/PrimeNumberTheoremAnd/ZetaBounds.lean index 20d8a329..a7c97980 100644 --- a/PrimeNumberTheoremAnd/ZetaBounds.lean +++ b/PrimeNumberTheoremAnd/ZetaBounds.lean @@ -730,13 +730,18 @@ with an absolute implied constant. lemma ZetaBnd_aux1b (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (σpos : 0 < σ) {t : ℝ} (ht : ct_aux1 < |t|) : ‖∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ ((σ + t * I) + 1)‖ ≤ C_aux1' * N ^ (-σ) / σ := by - have := @ZetaSum_aux1a (a := N) ?_ (by positivity) sorry ?_ sorry - have := @tendsto_nhds_unique (X := ℂ) (Y := ℕ) (l := atTop) - (f := fun k ↦ ((k : ℂ) ^ (1 - s) - (N : ℂ) ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑k ^ s) - 1 / 2 * (1 / ↑N ^ s) - + s * ∫ (x : ℝ) in (N : ℝ)..k, (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1))) - (b := (- N ^ (1 - s)) / (1 - s) - N ^ (-s) / 2 - + s * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1))) sorry +-- have := @MeasureTheory.intervalIntegral_tendsto_integral_Ioi (f := fun x ↦ (⌊x⌋ + 1 / 2 - x) / x ^ (σ + 1)) (a := N) (b := fun x ↦ (x : ℝ)) +-- (l := atTop) +-- -- (fun x ↦ (x : ℝ)) N atTop tendsto_coe_atTop +-- have := @le_of_tendsto +-- have := @ZetaSum_aux1a (a := N) ?_ (by positivity) sorry ?_ sorry +-- have := @tendsto_nhds_unique (X := ℂ) (Y := ℕ) (l := atTop) +-- (f := fun k ↦ ((k : ℂ) ^ (1 - s) - (N : ℂ) ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑k ^ s) - 1 / 2 * (1 / ↑N ^ s) +-- + s * ∫ (x : ℝ) in (N : ℝ)..k, (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1))) +-- (b := (- N ^ (1 - s)) / (1 - s) - N ^ (-s) / 2 +-- + s * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1))) + -- sorry /-%% \begin{proof}\uses{ZetaSum_aux1a} Apply Lemma \ref{ZetaSum_aux1a} with $a=N$ and $b\to \infty$. @@ -753,7 +758,7 @@ $$ as $|t|\to\infty$. \end{lemma} %%-/ -lemma ZetaBnd_aux1 (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (hσ : σ ∈ Ioc 0 2) : +lemma ZetaBnd_aux1 {N : ℕ} (Npos : 1 ≤ N) {σ : ℝ} (hσ : σ ∈ Ioc 0 2) : ∀ (t : ℝ) (_ : ct_aux1 < |t|), ‖(σ + t * I) * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ ((σ + t * I) + 1)‖ ≤ C_aux1 * |t| * N ^ (-σ) / σ := by @@ -763,19 +768,12 @@ lemma ZetaBnd_aux1 (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (hσ : σ ∈ Ioc 0 2) push_cast conv => rhs; lhs; lhs; rw [(by norm_num : (200 : ℝ) = 100 * 2), mul_assoc, mul_comm] rw [norm_mul, mul_assoc, mul_div_assoc] - apply mul_le_mul ?_ (ZetaBnd_aux1b N Npos hσ.1 t ht) (norm_nonneg _) (by positivity) - apply le_trans (b := ‖t + ↑t * I‖) - · simp only [norm_eq_abs, abs_eq_sqrt_sq_add_sq, add_re, ofReal_re, mul_re, I_re, mul_zero, - ofReal_im, I_im, mul_one, sub_self, add_zero, add_im, mul_im, zero_add] - apply Real.sqrt_le_sqrt - apply add_le_add_right <| sq_le_sq.mpr <| le_trans (b := 2) ?_ (by linarith) - simp only [mem_Ioc] at hσ; simp only [abs_of_pos hσ.1, hσ.2] - · simp only [norm_eq_abs, abs_eq_sqrt_sq_add_sq, add_re, ofReal_re, mul_re, I_re, mul_zero, - ofReal_im, I_im, mul_one, sub_self, add_zero, add_im, mul_im, zero_add] - ring_nf - simp only [Nat.ofNat_nonneg, Real.sqrt_mul', Real.sqrt_sq_eq_abs] - apply mul_le_mul_left (by linarith) |>.mpr - exact Real.sqrt_le_left (by norm_num) |>.mpr (by norm_num) + gcongr + · simp only [mem_Ioc] at hσ + calc _ ≤ ‖(σ : ℂ)‖ + ‖t * I‖ := norm_add_le .. + _ = |σ| + |t| := by simp + _ ≤ _ := by linarith [abs_of_pos hσ.1] + · exact ZetaBnd_aux1b N Npos hσ.1 ht /-%% \begin{proof}\uses{ZetaSum_aux1b}\leanok Apply Lemma \ref{ZetaSum_aux1b} and estimate $|s|\ll |t|$. From 74bf189841e30bb245106e5561bd55440e163e85 Mon Sep 17 00:00:00 2001 From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com> Date: Tue, 30 Apr 2024 11:25:54 -0400 Subject: [PATCH 3/7] fix --- PrimeNumberTheoremAnd/ZetaBounds.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PrimeNumberTheoremAnd/ZetaBounds.lean b/PrimeNumberTheoremAnd/ZetaBounds.lean index a7c97980..8f72e524 100644 --- a/PrimeNumberTheoremAnd/ZetaBounds.lean +++ b/PrimeNumberTheoremAnd/ZetaBounds.lean @@ -1203,7 +1203,7 @@ lemma ZetaUpperBnd : _ = _ := by ring · simp only [add_le_add_iff_right, one_div_cpow_eq_cpow_neg] convert UpperBnd_aux3 (C := 2) Apos (by norm_num) Npos σ_ge t_ge' N_le_t le_rfl - · simp only [add_le_add_iff_left]; exact ZetaBnd_aux1 N (by linarith) ⟨σPos, σ_le⟩ t t_ge + · simp only [add_le_add_iff_left]; exact ZetaBnd_aux1 (by linarith) ⟨σPos, σ_le⟩ t t_ge · simp only [norm_div, norm_neg, norm_eq_abs, RCLike.norm_ofNat, Nat.abs_cast, s] congr <;> (convert norm_natCast_cpow_of_pos Npos _; simp) · have ⟨h₁, h₂, h₃⟩ := UpperBnd_aux6 t_ge' σ_gt σ_le neOne Npos N_le_t From 8d6ff9c594f37711d4092008afd3fb21c812112d Mon Sep 17 00:00:00 2001 From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com> Date: Tue, 30 Apr 2024 12:18:44 -0400 Subject: [PATCH 4/7] integrableOn_of_Zeta0_fun change --- PrimeNumberTheoremAnd/ZetaBounds.lean | 71 ++++++++++++++++++++------- 1 file changed, 53 insertions(+), 18 deletions(-) diff --git a/PrimeNumberTheoremAnd/ZetaBounds.lean b/PrimeNumberTheoremAnd/ZetaBounds.lean index 8f72e524..cbee3b77 100644 --- a/PrimeNumberTheoremAnd/ZetaBounds.lean +++ b/PrimeNumberTheoremAnd/ZetaBounds.lean @@ -665,6 +665,17 @@ lemma ZetaSum_aux3 {N : ℕ} {s : ℂ} (s_re_gt : 1 < s.re) : · congr; ext n; simp only [one_div, Nat.cast_add, Nat.cast_one, f] · rwa [summable_nat_add_iff (k := 1)] +lemma 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))) (Ioi ↑N) + MeasureTheory.volume := by + apply MeasureTheory.Integrable.bdd_mul ?_ ?_ + · convert ZetaSum_aux2a; simp [← Complex.abs_ofReal] + · apply integrableOn_Ioi_cpow_iff (by positivity) |>.mpr (by simp [s_re_gt]) + · apply Measurable.aestronglyMeasurable + refine Measurable.sub (Measurable.add ?_ measurable_const) ?_ + · exact Measurable.comp (by exact fun _ _ ↦ trivial) Int.measurable_floor + · exact Measurable.comp measurable_id measurable_ofReal + /-%% \begin{lemma}[ZetaSum_aux2]\label{ZetaSum_aux2}\lean{ZetaSum_aux2}\leanok Let $N$ be a natural number and $s\in \C$, $\Re(s)>1$. @@ -700,13 +711,7 @@ lemma ZetaSum_aux2 {N : ℕ} (N_pos : 0 < N) {s : ℂ} (s_re_gt : 1 < s.re) : · simp_rw [mul_comm_div, one_mul, one_div, cpow_neg]; exact tendsto_const_nhds · refine MeasureTheory.intervalIntegral_tendsto_integral_Ioi (a := N) (b := (fun (n : ℕ) ↦ (n : ℝ))) ?_ tendsto_coe_atTop - apply MeasureTheory.Integrable.bdd_mul ?_ ?_ - · convert ZetaSum_aux2a; simp [← Complex.abs_ofReal] - · apply integrableOn_Ioi_cpow_iff (by positivity) |>.mpr (by simp [s_re_gt]; positivity) - · apply Measurable.aestronglyMeasurable - refine Measurable.sub (Measurable.add ?_ measurable_const) ?_ - · exact Measurable.comp (by exact fun _ _ ↦ trivial) Int.measurable_floor - · exact Measurable.comp measurable_id measurable_ofReal + exact integrableOn_of_Zeta0_fun N_pos (by linarith) /-%% \begin{proof}\uses{ZetaSum_aux1}\leanok Apply Lemma \ref{ZetaSum_aux1} with $a=N$ and $b\to \infty$. @@ -727,21 +732,51 @@ $$ with an absolute implied constant. \end{lemma} %%-/ +open MeasureTheory in lemma ZetaBnd_aux1b (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (σpos : 0 < σ) {t : ℝ} (ht : ct_aux1 < |t|) : ‖∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ ((σ + t * I) + 1)‖ ≤ C_aux1' * N ^ (-σ) / σ := by + have' lim1 := intervalIntegral_tendsto_integral_Ioi + (f := fun (x : ℝ) ↦ (⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ ((σ + t * I) + 1)) + (a := N) (b := fun x ↦ (x : ℝ)) + (l := atTop) (μ := volume) ?_ ?_ |>.norm +-- (fun x ↦ (x : ℝ)) N atTop tendsto_coe_atTop + convert le_of_tendsto lim1 (b := C_aux1' * N ^ (-σ) / σ) ?_ using 1 + · filter_upwards [Filter.mem_atTop (N + 1 : ℝ)] + intro b hb + have : (1 : ℝ) ≤ N := by exact_mod_cast Npos + have lim2 := @ZetaSum_aux1a (a := N) (b := b) (by linarith) + (by linarith) (s := σ + t * I) (by simp [σpos]) + calc _ ≤ _ := lim2 + _ ≤ _ := by + simp only [add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, + sub_self, add_zero] + gcongr + have : 0 < b ^ (- σ) := by + apply Real.rpow_pos_of_pos + linarith + have : 0 < (N : ℝ) ^ (- σ) := by + apply Real.rpow_pos_of_pos + linarith + rw [C_aux1'] + linarith + · have := integrableOn_of_Zeta0_fun (by linarith : 0 < N) (s := (σ + t * I + 1)) (by simp [σpos]) + convert this.congr_fun ?_ (by simp) + intro x hx + simp only [mem_Ioi] at hx + have xpos : 0 < x := by linarith + simp only + rw [div_eq_mul_inv (b := (x : ℂ) ^ (σ + t * I + 1)), Complex.cpow_neg] + congr! 3 + + + -- have := @ZetaSum_aux1a (a := N) ?_ (by positivity) sorry ?_ sorry + -- have := @tendsto_nhds_unique (X := ℂ) (Y := ℕ) (l := atTop) + -- (f := fun k ↦ ((k : ℂ) ^ (1 - s) - (N : ℂ) ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑k ^ s) - 1 / 2 * (1 / ↑N ^ s) + -- + s * ∫ (x : ℝ) in (N : ℝ)..k, (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1))) + -- (b := (- N ^ (1 - s)) / (1 - s) - N ^ (-s) / 2 + -- + s * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1))) sorry --- have := @MeasureTheory.intervalIntegral_tendsto_integral_Ioi (f := fun x ↦ (⌊x⌋ + 1 / 2 - x) / x ^ (σ + 1)) (a := N) (b := fun x ↦ (x : ℝ)) --- (l := atTop) --- -- (fun x ↦ (x : ℝ)) N atTop tendsto_coe_atTop --- have := @le_of_tendsto --- have := @ZetaSum_aux1a (a := N) ?_ (by positivity) sorry ?_ sorry --- have := @tendsto_nhds_unique (X := ℂ) (Y := ℕ) (l := atTop) --- (f := fun k ↦ ((k : ℂ) ^ (1 - s) - (N : ℂ) ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑k ^ s) - 1 / 2 * (1 / ↑N ^ s) --- + s * ∫ (x : ℝ) in (N : ℝ)..k, (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1))) --- (b := (- N ^ (1 - s)) / (1 - s) - N ^ (-s) / 2 --- + s * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1))) - -- sorry /-%% \begin{proof}\uses{ZetaSum_aux1a} Apply Lemma \ref{ZetaSum_aux1a} with $a=N$ and $b\to \infty$. From 0977ccb6c0eb5432191f663f1f2b64637aa324a0 Mon Sep 17 00:00:00 2001 From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com> Date: Tue, 30 Apr 2024 12:19:15 -0400 Subject: [PATCH 5/7] ZetaBnd_aux1b done --- PrimeNumberTheoremAnd/ZetaBounds.lean | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/PrimeNumberTheoremAnd/ZetaBounds.lean b/PrimeNumberTheoremAnd/ZetaBounds.lean index cbee3b77..be7c9b5e 100644 --- a/PrimeNumberTheoremAnd/ZetaBounds.lean +++ b/PrimeNumberTheoremAnd/ZetaBounds.lean @@ -760,23 +760,13 @@ lemma ZetaBnd_aux1b (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (σpos : 0 < σ) {t : linarith rw [C_aux1'] linarith - · have := integrableOn_of_Zeta0_fun (by linarith : 0 < N) (s := (σ + t * I + 1)) (by simp [σpos]) + · have := integrableOn_of_Zeta0_fun (by linarith : 0 < N) (s := (σ + t * I)) (by simp [σpos]) convert this.congr_fun ?_ (by simp) intro x hx simp only [mem_Ioi] at hx have xpos : 0 < x := by linarith simp only rw [div_eq_mul_inv (b := (x : ℂ) ^ (σ + t * I + 1)), Complex.cpow_neg] - congr! 3 - - - -- have := @ZetaSum_aux1a (a := N) ?_ (by positivity) sorry ?_ sorry - -- have := @tendsto_nhds_unique (X := ℂ) (Y := ℕ) (l := atTop) - -- (f := fun k ↦ ((k : ℂ) ^ (1 - s) - (N : ℂ) ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑k ^ s) - 1 / 2 * (1 / ↑N ^ s) - -- + s * ∫ (x : ℝ) in (N : ℝ)..k, (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1))) - -- (b := (- N ^ (1 - s)) / (1 - s) - N ^ (-s) / 2 - -- + s * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1))) - sorry /-%% \begin{proof}\uses{ZetaSum_aux1a} Apply Lemma \ref{ZetaSum_aux1a} with $a=N$ and $b\to \infty$. From 7bf3e44af52afa14e72125e0071473e4016a50ab Mon Sep 17 00:00:00 2001 From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com> Date: Tue, 30 Apr 2024 12:21:30 -0400 Subject: [PATCH 6/7] ZetaBnd_aux1b fix --- PrimeNumberTheoremAnd/ZetaBounds.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/PrimeNumberTheoremAnd/ZetaBounds.lean b/PrimeNumberTheoremAnd/ZetaBounds.lean index be7c9b5e..9b508cfb 100644 --- a/PrimeNumberTheoremAnd/ZetaBounds.lean +++ b/PrimeNumberTheoremAnd/ZetaBounds.lean @@ -733,14 +733,13 @@ with an absolute implied constant. \end{lemma} %%-/ open MeasureTheory in -lemma ZetaBnd_aux1b (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (σpos : 0 < σ) {t : ℝ} (ht : ct_aux1 < |t|) : +lemma ZetaBnd_aux1b (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (σpos : 0 < σ) {t : ℝ} : ‖∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ ((σ + t * I) + 1)‖ ≤ C_aux1' * N ^ (-σ) / σ := by have' lim1 := intervalIntegral_tendsto_integral_Ioi (f := fun (x : ℝ) ↦ (⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ ((σ + t * I) + 1)) (a := N) (b := fun x ↦ (x : ℝ)) (l := atTop) (μ := volume) ?_ ?_ |>.norm --- (fun x ↦ (x : ℝ)) N atTop tendsto_coe_atTop convert le_of_tendsto lim1 (b := C_aux1' * N ^ (-σ) / σ) ?_ using 1 · filter_upwards [Filter.mem_atTop (N + 1 : ℝ)] intro b hb @@ -764,9 +763,9 @@ lemma ZetaBnd_aux1b (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (σpos : 0 < σ) {t : convert this.congr_fun ?_ (by simp) intro x hx simp only [mem_Ioi] at hx - have xpos : 0 < x := by linarith simp only rw [div_eq_mul_inv (b := (x : ℂ) ^ (σ + t * I + 1)), Complex.cpow_neg] + · exact fun ⦃U⦄ a ↦ a /-%% \begin{proof}\uses{ZetaSum_aux1a} Apply Lemma \ref{ZetaSum_aux1a} with $a=N$ and $b\to \infty$. @@ -798,7 +797,7 @@ lemma ZetaBnd_aux1 {N : ℕ} (Npos : 1 ≤ N) {σ : ℝ} (hσ : σ ∈ Ioc 0 2) calc _ ≤ ‖(σ : ℂ)‖ + ‖t * I‖ := norm_add_le .. _ = |σ| + |t| := by simp _ ≤ _ := by linarith [abs_of_pos hσ.1] - · exact ZetaBnd_aux1b N Npos hσ.1 ht + · exact ZetaBnd_aux1b N Npos hσ.1 /-%% \begin{proof}\uses{ZetaSum_aux1b}\leanok Apply Lemma \ref{ZetaSum_aux1b} and estimate $|s|\ll |t|$. From 714b6268d7c2191e093c80bea35bbf1cccb4ba03 Mon Sep 17 00:00:00 2001 From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com> Date: Tue, 30 Apr 2024 12:24:53 -0400 Subject: [PATCH 7/7] blueprint --- PrimeNumberTheoremAnd/ZetaBounds.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/PrimeNumberTheoremAnd/ZetaBounds.lean b/PrimeNumberTheoremAnd/ZetaBounds.lean index 9b508cfb..30fd4f3f 100644 --- a/PrimeNumberTheoremAnd/ZetaBounds.lean +++ b/PrimeNumberTheoremAnd/ZetaBounds.lean @@ -767,7 +767,7 @@ lemma ZetaBnd_aux1b (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (σpos : 0 < σ) {t : rw [div_eq_mul_inv (b := (x : ℂ) ^ (σ + t * I + 1)), Complex.cpow_neg] · exact fun ⦃U⦄ a ↦ a /-%% -\begin{proof}\uses{ZetaSum_aux1a} +\begin{proof}\uses{ZetaSum_aux1a}\leanok Apply Lemma \ref{ZetaSum_aux1a} with $a=N$ and $b\to \infty$. \end{proof} %%-/ @@ -845,6 +845,7 @@ lemma HolomorphicOn_riemannZeta0 {N : ℕ} (N_pos : 0 < N) : · fun_prop · norm_num · apply DifferentiableOn.mul differentiableOn_id + --extract_goal sorry /-%% \begin{proof}\uses{ZetaSum_aux1, ZetaBnd_aux1b}