ZetaInvBound1

@[blueprint  (title := "ZetaInvBound1")  (statement := /--  For all $\sigma>1$,  $$  1/|\zeta(\sigma+it)| \le |\zeta(\sigma)|^{3/4}|\zeta(\sigma+2it)|^{1/4}  $$  -/)  (proof := /--  The identity  $$  1 \le |\zeta(\sigma)|^3 |\zeta(\sigma+it)|^4 |\zeta(\sigma+2it)|  $$  for $\sigma>1$  is already proved by Michael Stoll in the EulerProducts PNT file.  -/)  (latexEnv := "lemma")]lemma ZetaInvBound1 {σ t : ℝ} (σ_gt : 1 < σ) :    1 / ‖ζ (σ + t * I)‖ ≤ ‖ζ σ‖ ^ ((3 : ℝ) / 4) * ‖ζ (σ + 2 * t * I)‖ ^ ((1 : ℝ) / 4) := by  apply (div_le_iff₀ ?_).mpr  · apply (Real.rpow_le_rpow_iff (z := 4) (by norm_num) ?_ (by norm_num)).mp    · simp only [Real.one_rpow]      rw [Real.mul_rpow, Real.mul_rpow, ← Real.rpow_mul, ← Real.rpow_mul]      · simp only [isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,          IsUnit.div_mul_cancel, Real.rpow_one]        conv => rw [mul_assoc]; rhs; rhs; rw [mul_comm]        rw [← mul_assoc]        have := norm_zeta_product_ge_one (x := σ - 1) (by linarith) t        simp_rw [ge_iff_le, norm_mul, norm_pow, ofReal_sub, ofReal_one, add_sub_cancel, ← Real.rpow_natCast] at this        convert this using 3 <;> ring_nf      any_goals ring_nf      any_goals apply norm_nonneg      any_goals apply Real.rpow_nonneg <| norm_nonneg _      apply mul_nonneg <;> apply Real.rpow_nonneg <| norm_nonneg _    · refine mul_nonneg (mul_nonneg ?_ ?_) ?_ <;> simp [Real.rpow_nonneg]  · have s_ne_one : σ + t * I ≠ 1 := by      contrapose! σ_gt; apply le_of_eq; apply And.left; simpa [Complex.ext_iff] using σ_gt    simpa using riemannZeta_ne_zero_of_one_le_re (by simp [σ_gt.le])