From 58eff5fa88120cef0da3751a72d7dcfeb6f4b00c Mon Sep 17 00:00:00 2001
From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com>
Date: Mon, 6 May 2024 10:51:23 -0700
Subject: [PATCH] ZetaInvBnd to  be refactored

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

diff --git a/PrimeNumberTheoremAnd/ZetaBounds.lean b/PrimeNumberTheoremAnd/ZetaBounds.lean
index 422aaefd..2b4ba381 100644
--- a/PrimeNumberTheoremAnd/ZetaBounds.lean
+++ b/PrimeNumberTheoremAnd/ZetaBounds.lean
@@ -1740,7 +1740,15 @@ lemma ZetaInvBnd :
     sorry
   refine ⟨A, ⟨Apos, by linarith [hA'.2]⟩ , C, Cpos, ?_⟩
   intro σ t t_gt hσ
+
+  sorry
+
+#exit
+
   have logt_gt_one := logt_gt_one t_gt
+
+
+
   have σ_ge : 1 - A / |t|.log ≤ σ := by
     apply le_trans ?_ hσ.1
     suffices A / |t|.log ^ 9 ≤ A / |t|.log by linarith