ZetaLowerBound3

@[blueprint  (title := "ZetaLowerBound3")  (statement := /--  There exists a $c>0$ such that for all $1 < \sigma <= 2$ and $3 < |t|$,  $$  c \frac{(\sigma-1)^{3/4}}{(\log |t|)^{1/4}} \le |\zeta(\sigma + tI)|.  $$  -/)  (proof := /--  Combine Lemma \ref{ZetaLowerBound2} with upper bounds for  $|\zeta(\sigma)|$ (from Lemma \ref{ZetaNear1BndExact}) and  $|\zeta(\sigma+2it)|$ (from Lemma \ref{ZetaUpperBnd}).  -/)  (latexEnv := "lemma")]lemma ZetaLowerBound3 :    ∃ c > 0, ∀ {σ : ℝ} (_ : σ ∈ Ioc 1 2) (t : ℝ) (_ : 3 < |t|),    c * (σ - 1) ^ ((3 : ℝ) / 4) / (Real.log |t|) ^ ((1 : ℝ) / 4) ≤ ‖ζ (σ + t * I)‖ := by  obtain ⟨A, ha, C, hC, h_upper⟩ := ZetaUpperBnd  obtain ⟨c_near, hc_near, h_near⟩ := ZetaNear1BndExact   use 1 / (c_near ^ ((3 : ℝ) / 4) * (2 * C) ^ ((1 : ℝ) / 4)), by positivity  intro σ hσ t ht  obtain ⟨σ_gt, σ_le⟩ := hσ   -- Use ZetaLowerBound2  have lower := ZetaLowerBound2 (t := t) σ_gt  apply le_trans _ lower   -- Now we need to bound the denominator from above  -- This will give us a lower bound on the whole expression   -- Upper bound on ‖ζ σ‖ from ZetaNear1BndExact  have ζ_σ_bound : ‖ζ σ‖ ≤ c_near / (σ - 1) := by    exact h_near σ ⟨σ_gt, σ_le⟩   have ht_2 : 3 < |2 * t| := by simp only [abs_mul, Nat.abs_ofNat]; linarith   -- Upper bound on ‖ζ (σ + 2*t * I)‖ from ZetaUpperBnd   have σ_in_range : σ ∈ Icc (1 - A / Real.log |2 * t|) 2 := by    constructor    · -- σ ≥ 1 - A / Real.log |2*t|      have : 0 < A / Real.log |2 * t| := by        exact ZetaLowerBound3_aux1 A ha t ht_2      nlinarith    · exact σ_le   have ζ_2t_bound := h_upper σ (2 * t) ht_2 σ_in_range   -- Combine the bounds  have denom_bound : ‖ζ σ‖ ^ ((3 : ℝ) / 4) * ‖ζ (σ + 2 * t * I)‖ ^ ((1 : ℝ) / 4) ≤      (c_near / (σ - 1)) ^ ((3 : ℝ) / 4) * (C * Real.log |2 * t|) ^ ((1 : ℝ) / 4) := by    apply mul_le_mul    · apply Real.rpow_le_rpow (norm_nonneg _) ζ_σ_bound (by norm_num)    · apply ZetaLowerBound3_aux2      convert ζ_2t_bound      norm_cast    · apply Real.rpow_nonneg (norm_nonneg _)    · apply Real.rpow_nonneg (div_nonneg (by linarith) (by linarith))   -- Simplify the bound  have : (c_near / (σ - 1)) ^ ((3 : ℝ) / 4) * (C * Real.log |2 * t|) ^ ((1 : ℝ) / 4) =         c_near ^ ((3 : ℝ) / 4) * (σ - 1) ^ (-(3 : ℝ) / 4) * C ^ ((1 : ℝ) / 4) * (Real.log |2 * t|) ^ ((1 : ℝ) / 4) := by    rw [Real.div_rpow (by linarith) (by linarith), Real.mul_rpow (by linarith) (Real.log_nonneg (by linarith))]    ring_nf    exact ZetaLowerBound3_aux3 _ _ _ σ_gt  rw [this] at denom_bound   -- Take reciprocal (flipping inequality)  have pos_left : 0 < c_near ^ ((3 : ℝ) / 4) * (σ - 1) ^ (-(3 : ℝ) / 4) * C ^ ((1 : ℝ) / 4) * (Real.log |2 * t|) ^ ((1 : ℝ) / 4) := by    apply ZetaLowerBound3_aux4 C hC c_near hc_near t ht σ_gt   have pos_right : 0 < ‖ζ σ‖ ^ ((3 : ℝ) / 4) * ‖ζ (σ + 2 * t * I)‖ ^ ((1 : ℝ) / 4) := by    -- This follows from ZetaLowerBound1 - if either factor were zero, we'd get 0 ≥ 1    apply ZetaLowerBound3_aux5 _ <| ZetaLowerBound1 (t := t) σ_gt    use (div_le_div_of_nonneg_left zero_le_one pos_right denom_bound).trans' ?_  simp_rw [abs_mul, abs_two, neg_div, Real.rpow_neg (sub_pos.2 σ_gt).le] at *  have hlog : 0 < Real.log |t| := Real.log_pos <| ht.trans' <| by norm_num  have : 0 < Real.log |t| ^ (1 / 4 : ℝ) := Real.rpow_pos_of_pos hlog _  have hlog2 : 0 < Real.log (2 * |t|) := Real.log_pos <| ht_2.trans' <| by norm_num  have : 0 < Real.log (2 * |t|) ^ (1 / 4 : ℝ) := Real.rpow_pos_of_pos hlog2 (1 / 4)  field_simp  rw [Real.mul_rpow two_pos.le hC.le]  move_mul [C ^ (1 / 4)]  rw [mul_le_mul_iff_left₀]  swap  · positivity  rw [← Real.mul_rpow two_pos.le hlog.le]  apply Real.rpow_le_rpow hlog2.le ?_ (by norm_num)  rw [← Real.log_rpow (ht.trans' (by norm_num))]  apply Real.log_le_log (ht_2.trans' (by norm_num))  rw [Real.rpow_two, sq]  gcongr  exact ht.trans' (by norm_num) |>.le