ZetaInvBnd to be refactored

AlexKontorovich · May 6, 2024 · 58eff5f · 58eff5f
1 parent 43455aa
commit 58eff5f
Showing 1 changed file with 8 additions and 0 deletions.
diff --git 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