From 43455aa0f9b11f8bc09ff6561ab33833db795f82 Mon Sep 17 00:00:00 2001
From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com>
Date: Mon, 6 May 2024 10:48:32 -0700
Subject: [PATCH] ZetaInvBnd work

---
 PrimeNumberTheoremAnd/ZetaBounds.lean | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/PrimeNumberTheoremAnd/ZetaBounds.lean b/PrimeNumberTheoremAnd/ZetaBounds.lean
index 58a2b317..422aaefd 100644
--- a/PrimeNumberTheoremAnd/ZetaBounds.lean
+++ b/PrimeNumberTheoremAnd/ZetaBounds.lean
@@ -1730,11 +1730,15 @@ lemma ZetaInvBnd :
     (hσ : σ ∈ Ico (1 - A / (Real.log |t|) ^ 9) 1),
     1 / ‖ζ (σ + t * I)‖ ≤ C * (Real.log |t|) ^ 7 := by
   obtain ⟨A', hA', C', hC', h'⟩ := Zeta_diff_Bnd
-  let A := min A' <| (1 / 16 : ℝ)
+  obtain ⟨C₂, C₂pos, hC'⟩ := ZetaInvBound2
+  let A := min A' <| (1 / 2 : ℝ) * (C' / 2 * C₂) ^ 4
   have Apos : 0 < A := by have := hA'.1; positivity
-  let C := C'
-  have Cpos : 0 < C := by positivity
-  refine ⟨A, ⟨Apos, by norm_num [A]⟩ , C, Cpos, ?_⟩
+  have A_le_A' : A ≤ A' := by simp [A]
+  let C := C' * A ^ (3 / 4 : ℝ) - 2 * A * C₂
+  have Cpos : 0 < C := by
+    apply sub_pos.mpr
+    sorry
+  refine ⟨A, ⟨Apos, by linarith [hA'.2]⟩ , C, Cpos, ?_⟩
   intro σ t t_gt hσ
   have logt_gt_one := logt_gt_one t_gt
   have σ_ge : 1 - A / |t|.log ≤ σ := by