[{"type":"thinking","thinking":"Committed (1c76576). Now c-ii: `digamma_right_le` + `digamma_circle_le` + small elems.\n\n1. `digamma_right_le {w : ℂ} (hwre : (1.75:ℝ) ≤ w.re) : ‖Complex.digamma w‖ ≤ 48 + 23 * Real.log (2 + ‖w‖)`.\n\n2. `digamma_circle_le {s : ℂ} (hs : ‖s‖ = R) (hgapInt : ∀ m : ℤ, 1/4 ≤ |R/2 − (m:ℝ)|) (hR : (16002:ℝ) ≤ R) : ‖Complex.digamma (s/2)‖ ≤ 62 + 23 * Real.log (2 + R/2)`.\nCases:\n(a) 5 ≤ |im(s/2)|: sub-log: norm_digamma_sub_log_le_of_two_le_abs_im (2 ≤ |im(s/2)|) + norm_log_le_of_one_le (‖s/2‖ = R/2 ≥ 1): ‖ψ(s/2)‖ ≤ 3 + (log‖s/2‖ + π) = 3 + log(R/2) + π ≤ 62 + 23·log(2+R/2): log(R/2) ≤ log(2+R/2) ✓; 3+π ≤ 7 ≤ 62·... need 3 + log(R/2) + π ≤ 62 + 23·log(2+R/2): from log(R/2) ≤ log(2+R/2) and 3+π ≤ 62 + 22·log(2+R/2) (22·log(2+R/2) ≥ 0 ⟹ RHS ≥ 62 ≥ 7 ✓... 62 + 23·log ≥ 62 ≥ 3+π + log(R/2)−log(2+R/2)·... hmm: 3 + log(R/2) + π vs 62 + 23·log(2+R/2): split: log(R/2) ≤ log(2+R/2) (mono, R/2 ≤ 2+R/2 ✓, R/2 > 0) and 3+π ≤ 62 + 22·log(2+R/2) ⟸ 22·log(2+R/2) ≥ 0 and 3+π ≤ 62 ⟸ π ≤ 59 ⟸ pi_lt_315 (3.15) ✓. linarith with those two haves ✓.\n(b) |im(s/2)| < 5 ∧ 1.75 ≤ re(s/2): digamma_right_le: ≤ 48 + 23·log(2+‖s/2‖) = 48 + 23·log(2+R/2) ≤ 62 + ... ✓ (‖s/2‖ = R/2).\n(c) |im(s/2)| < 5 ∧ re(s/2) < 1.75: the left dist case: \n   - re(s/2) < 0: |im s| = 2·|im(s/2)| < 10: (re s)² = R² − (im s)² > R² − 100: |re s| > R − 100/R (from (R−|re s|)(R+|re s|) = (im s)² < 100 ⟹ R−|re s| < 100/(R+|re s|) ≤ 100/R): so |re(s/2)| = |re s|/2 > R/2 − 50/R ≥ R/2 − 1 (50/R < 1 ⟺ R > 50 ✓): with re(s/2) < 1.75: re(s/2) ∈ (−R/2, −(R/2−50/R)) hmm: |re(s/2)| > R/2 − 50/R: either re(s/2) > R/2−50/R ≥ 1.75 (contradiction with < 1.75 since R/2−50/R ≥ R/2−1 ≥ 8000) or re(s/2) < −(R/2−50/R): hence re(s/2) < 0 and (re s)/2 + R/2 ∈ [0, 50/R): (re s)/2 ≥ −R/2 ⟹ ≥ 0 ✓; (re s)/2 < −R/2 + 50/R ⟹ < 50/R ✓.\n   - dist: ∀ m : ℕ, 1/8 ≤ ‖s/2 + (m:ℂ)‖: ‖s/2+m‖ ≥ |(s/2+m).re| = |(re s)/2 + m|: (re s)/2 + m = ((re s)/2 + R/2) + (m − R/2): |(re s)/2 + m| ≥ |m − R/2| − ((re s)/2 + R/2) ≥ 1/4 − 50/R ≥ 1/8 (50/R ≤ 1/8 ⟺ 400 ≤ R ✓): |m − R/2| = |R/2 − (m:ℤ)| ≥ 1/4 by hgapInt ((m : ℤ)) — cast: |R/2 − ((m:ℤ):ℝ)| with (m:ℤ) = m ✓ push_cast. And reverse triangle: |a + b| ≥ |a| − |b| hmm: (re s)/2 + m = (m − R/2) + ((re s)/2 + R/2): |X + Y| ≥ |X| − |Y| (abs_sub_abs_le_abs_sub X (−Y)? |X| − |Y| ≤ |X + Y| ✓ via |X| = |X+Y−Y| ≤ |X+Y|+|Y| ✓ linarith-friendly: have := abs_sub_abs_le_abs_sub (m − R/2) (-((re s)/2 + R/2))... simpler: |X+Y| ≥ |X|−|Y| is `abs_sub_abs_le_abs_sub X (-Y) : |(|X| − |−Y|)| ≤ |X−(−Y)| = |X+Y|`: |X|−|Y| ≤ ||X|−|Y|| ≤ |X+Y| ✓ chain via abs_le.mp or le_abs_self. Fine with linarith [abs_abs_sub_abs_le_abs_sub X (-Y), le_abs_self (|X|−|Y|)] hmm — |(|X|−|−Y|)| ≤ |X+Y| and |X|−|Y| ≤ |(|X|−|−Y|)| (le_abs_self) and |−Y| = |Y| (abs_neg): linarith ✓.\n   - then (A): norm_digamma_le_of_dist_nat (c := 1/8, hc : 0 < 1/8) (hwre : (s/2).re ≤ 2 — re(s/2) < 0 ≤ 2 ✓) hdist: ‖ψ(s/2)‖ ≤ (46 + 2/(1/8)) + 23·log(2+‖s/2‖) = (46+16) + 23·log(2+R/2) = 62 + 23·log(2+R/2) ✓ EXACT.\n   Need (s/2).re = s.re/2: simp [Complex.div_re, Complex.ofNat_re]?? re(s/2): s/2 = s * (1/2)? or HDiv: (s/2).re = s.re/2: `Complex.div_re : (x / y).re = x.re / y.re - x.im / y.im`?? for complex division! s/2 as complex division: (s/2).re = (s.re·2 + s.im·0)/(2²) = s.re/2 — messy via div_re. Better: ofNat division: `Complex.div_ofNat_re : (x / n).re = x.re / n`?? There's `Complex.div_ofNat_re (z : ℂ) (n : ℕ) : (z / (n:ℂ)).re = z.re / n`?? Hmm — there might be `Complex.ofNat_div_re`? Let me just use: s/2 = s * (2:ℂ)⁻¹: (s * (2:ℂ)⁻¹).re = s.re·(2⁻¹).re − s.im·(2⁻¹).im = s.re·(1/2): via Complex.mul_re + ofReal_inv... Simplest robust: have : (s / 2).re = s.re / 2 := by simp [Complex.div_re, Complex.ofNat_re] — try it; if simp doesn't fully close, ext via: `Complex.ext_iff`? Actually there's a cleaner lemma: `Complex.div_ofNat_re : (z / ofNat n).re = z.re / ofNat n`? I recall `Complex.div_ofNat_re` and `Complex.div_ofNat_im` exist in Mathlib (for OfNat.ofNat numerals). Try simp first.\n\n3. Small elems:\n- `norm_one_div_of_norm_eq {s : ℂ} {R : ℝ} (hs : ‖s‖ = R) (hR : 1 ≤ R) : ‖(1:ℂ)/s‖ ≤ 1`: ‖1/s‖ = 1/‖s‖ = 1/R ≤ 1: norm_div, norm_one, div_le_one.\n- `norm_one_div_sub_one_circle_le {s : ℂ} {R : ℝ} (hs : ‖s‖ = R) (hR : 2 ≤ R) : ‖(1:ℂ)/(s−1)‖ ≤ 1`: ‖s−1‖ ≥ R−1 ≥ 1: 1/‖s−1‖ ≤ 1.\n- `log_pi_le_two : Real.log Real.pi ≤ 2`: π ≤ e²: Real.pi_lt_315 hmm: π < 3.15 ≤ (2.7)² = 7.29 ≤ e² (e² ≥ 2.7²): Real.log_le_log Real.pi_pos: log π ≤ log(e²) = 2.\n- `norm_logPi_div_two_le : ‖(Real.log Real.pi : ℂ)/2‖ ≤ 1`: norm_div, RCLike.norm_ofReal?? ‖(x:ℂ)‖ = |x|: `Complex.norm_ofReal`? The name: `Complex.norm_ofReal : ‖(x : ℂ)‖ = |x|`? or `RCLike.norm_ofReal`. Then |log π|/2 ≤ 1 (log π ∈ (0, 2]: Real.log_pos (pi > 1)). \n\nLet me write c-ii now.","signature":""},{"type":"text","text":"Committed. Now c-ii: the digamma bounds + small elems."},{"type":"tool_use","id":"Edit_178","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-! ## 11. The digamma bounds and the elementary terms (5e-v-c-ii)\n\n`digamma_right_le`: re w ≥ 1.75 ⟹ ‖ψ(w)‖ ≤ 48 + 23·log(2+‖w‖)\n(sub-log for |im| ≥ 5; 5e-ii (B) for re ≥ 2; 5e-ii (A) with c = 1\nelse). `digamma_circle_le`: on the gap circle, ‖ψ(s/2)‖ ≤\n62 + 23·log(2+R/2) UNIFORMLY (strip arcs: sub-log; re(s/2) ≥ 1.75:\nright_le; the left near-axis: 5e-ii (A) with c = 1/8 from the\nℤ-clearance dist(R/2,ℤ) ≥ 1/4 — the R+re s = im²/(R−re s) identity\navoids square roots). Small elems: ‖1/s‖, ‖1/(s−1)‖, ‖(log π)/2‖. -/\n\n/-- The right-halfplane digamma bound: re w ≥ 1.75 ⟹\n‖ψ(w)‖ ≤ 48 + 23·log(2+‖w‖). -/\nlemma digamma_right_le {w : ℂ} (hwre : (1.75 : ℝ) ≤ w.re) :\n    ‖Complex.digamma w‖ ≤ 48 + 23 * Real.log (2 + ‖w‖) := by\n  have hlog2w_nn : (0 : ℝ) ≤ Real.log (2 + ‖w‖) :=\n    Real.log_nonneg (by linarith [norm_nonneg w] : (1 : ℝ) ≤ 2 + ‖w‖)\n  rcases le_or_gt (5 : ℝ) |w.im| with him | him\n  · -- the Stirling-flavoured sub-log bound\n    have h1 := norm_digamma_sub_log_le_of_two_le_abs_im (by linarith [him] : (2 : ℝ) ≤ |w.im|)\n    have hwnorm : (1 : ℝ) ≤ ‖w‖ := by\n      have h2 := Complex.abs_re_le_norm w\n      rw [abs_of_nonneg (by linarith [hwre])] at h2\n      linarith [hwre, h2]\n    have h2 := norm_log_le_of_one_le hwnorm\n    have hlogle : Real.log ‖w‖ ≤ Real.log (2 + ‖w‖) :=\n      Real.log_le_log (by linarith [hwnorm] : (0 : ℝ) < ‖w‖)\n        (by linarith [norm_nonneg w])\n    have hpi : Real.pi ≤ 45 := by have h := Real.pi_lt_315; linarith\n    calc ‖Complex.digamma w‖\n        = ‖(Complex.digamma w - Complex.log w) + Complex.log w‖ := by rw [sub_add_cancel]\n      _ ≤ ‖Complex.digamma w - Complex.log w‖ + ‖Complex.log w‖ := norm_add_le _ _\n      _ ≤ 3 + (Real.log ‖w‖ + Real.pi) := add_le_add h1 h2\n      _ ≤ 48 + 23 * Real.log (2 + ‖w‖) := by linarith [hlogle, hpi, hlog2w_nn]\n  · by_cases hwre2 : (2 : ℝ) ≤ w.re\n    · -- 5e-ii (B)\n      have h1 := norm_digamma_le_of_two_le_re hwre2 (by linarith [him])\n      linarith [h1, hlog2w_nn]\n    · -- 5e-ii (A) with c = 1\n      push Not at hwre2\n      have hdist : ∀ m : ℕ, (1 : ℝ) ≤ ‖w + (m : ℂ)‖ := by\n        intro m\n        have h1 : ‖w + (m : ℂ)‖ ≥ |(w + (m : ℂ)).re| := Complex.abs_re_le_norm _\n        have h2 : (w + (m : ℂ)).re = w.re + (m : ℝ) := by\n          rw [Complex.add_re, Complex.natCast_re]\n        rw [h2] at h1\n        have h3 : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg _\n        linarith [hwre, h1, h3]\n      have h1 := norm_digamma_le_of_dist_nat (show (0 : ℝ) < 1 by norm_num)\n        (by linarith [hwre2] : w.re ≤ 2) hdist\n      have h2 : (46 : ℝ) + 2 / 1 = 48 := by norm_num\n      rw [h2] at h1\n      exact h1\n\n/-- **The uniform digamma bound on the gap circle**: ‖ψ(s/2)‖ ≤\n62 + 23·log(2+R/2). -/\nlemma digamma_circle_le {s : ℂ} {R : ℝ} (hs : ‖s‖ = R)\n    (hgapInt : ∀ m : ℤ, 1 / 4 ≤ |R / 2 - (m : ℝ)|) (hR : (16002 : ℝ) ≤ R) :\n    ‖Complex.digamma (s / 2)‖ ≤ 62 + 23 * Real.log (2 + R / 2) := by\n  have hRpos : (0 : ℝ) < R := by linarith [hR]\n  have hsnorm : ‖s / 2‖ = R / 2 := by\n    rw [norm_div, hs]\n    have h1 : ‖(2 : ℂ)‖ = 2 := by\n      rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n      norm_num\n    rw [h1]\n  have hre : (s / 2).re = s.re / 2 := by simp [Complex.div_re, Complex.ofNat_re]\n  have hlog_nn : (0 : ℝ) ≤ Real.log (2 + R / 2) :=\n    Real.log_nonneg (by linarith [hRpos] : (1 : ℝ) ≤ 2 + R / 2)\n  have him2 : (s / 2).im = s.im / 2 := by simp [Complex.div_im, Complex.ofNat_im]\n  rcases le_or_gt (5 : ℝ) |(s / 2).im| with him | him\n  · -- strip arcs: the sub-log bound\n    have h1 := norm_digamma_sub_log_le_of_two_le_abs_im (by linarith [him] :\n      (2 : ℝ) ≤ |(s / 2).im|)\n    have hwnorm : (1 : ℝ) ≤ ‖s / 2‖ := by rw [hsnorm]; linarith [hR]\n    have h2 := norm_log_le_of_one_le hwnorm\n    have hlogle : Real.log (R / 2) ≤ Real.log (2 + R / 2) :=\n      Real.log_le_log (by linarith [hRpos] : (0 : ℝ) < R / 2) (by linarith [hRpos])\n    have hpi : Real.pi ≤ 45 := by have h := Real.pi_lt_315; linarith\n    rw [hsnorm] at h2\n    calc ‖Complex.digamma (s / 2)‖\n        = ‖(Complex.digamma (s / 2) - Complex.log (s / 2)) + Complex.log (s / 2)‖ := by\n          rw [sub_add_cancel]\n      _ ≤ ‖Complex.digamma (s / 2) - Complex.log (s / 2)‖ + ‖Complex.log (s / 2)‖ :=\n          norm_add_le _ _\n      _ ≤ 3 + (Real.log (R / 2) + Real.pi) := add_le_add h1 h2\n      _ ≤ 62 + 23 * Real.log (2 + R / 2) := by linarith [hlogle, hpi, hlog_nn]\n  · by_cases hre2 : (1.75 : ℝ) ≤ (s / 2).re\n    · -- the right bound (48 ≤ 62)\n      have h1 := digamma_right_le hre2\n      rw [hsnorm] at h1\n      linarith [h1, hlog_nn]\n    · -- the left near-axis: 5e-ii (A) with c = 1/8\n      push Not at hre2\n      have him10 : |s.im| < 10 := by\n        rw [him2] at him\n        have h1 : |s.im / 2| = |s.im| / 2 := by\n          rw [abs_div, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 2)]\n        linarith [him, h1]\n      -- (re s)² = R² − (im s)² > R²−100 ⟹ |re s| > R−100/R\n      have hnormSq : ‖s‖ ^ 2 = s.re ^ 2 + s.im ^ 2 := by\n        rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n        ring\n      have himsq : s.im ^ 2 < 100 := by nlinarith [him10, abs_nonneg s.im]\n      have hre2sq : s.re ^ 2 = R ^ 2 - s.im ^ 2 := by\n        have h1 : s.re ^ 2 + s.im ^ 2 = R ^ 2 := by rw [← hnormSq, hs]\n        linarith\n      have hRmin : R - |s.re| < 100 / R := by\n        have h1 : (R - |s.re|) * (R + |s.re|) = s.im ^ 2 := by\n          have h2 : (R - |s.re|) * (R + |s.re|) = R ^ 2 - |s.re| ^ 2 := by ring\n          rw [h2, sq_abs]\n          linarith [hre2sq]\n        have h2 : R + |s.re| ≥ R := by\n          have h3 : (0 : ℝ) ≤ |s.re| := abs_nonneg _\n          linarith\n        have h3 : (R - |s.re|) * (R + |s.re|) < 100 := by linarith [h1, himsq]\n        have h4 : (0 : ℝ) < R + |s.re| := by linarith [hRpos, abs_nonneg s.re]\n        have h5 : (R - |s.re|) * (R + |s.re|) ≥ (R - |s.re|) * R :=\n          mul_le_mul_of_nonneg_left h2 (by\n            have h6 := abs_norm_sub_norm_le s (1 : ℂ)\n            rw [hs, norm_one] at h6\n            have h7 : R - 1 ≤ |R - 1| := le_abs_self _\n            have h8 : |R - ‖(1 : ℂ)‖| ≤ ‖s - (1 : ℂ)‖ := h6\n            -- R − |re s| ≥ 0 since |re s| ≤ R\n            have h9 : |s.re| ≤ R := by\n              have h10 := abs_re_le_norm s\n              rw [hs] at h10\n              exact h10\n            linarith [h9])\n        have h6 : (R - |s.re|) * R < 100 := by linarith [h3, h5]\n        exact (mul_lt_mul_right hRpos).mp (by linarith [h6] :\n          (R - |s.re|) * R < 100)\n      -- re(s/2) + R/2 ∈ [0, 50/R)\n      have hre_neg : (s / 2).re < 0 := by\n        have h9 : |s.re| ≤ R := by\n          have h10 := abs_re_le_norm s\n          rw [hs] at h10\n          exact h10\n        have h10 : |s.re| > R - 100 / R := by\n          have h11 : (0 : ℝ) ≤ |s.re| := abs_nonneg _\n          have h12 : R - |s.re| < 100 / R := hRmin\n          have h13 : |s.re| ≥ 0 := h11\n          by_cases hsign : 0 ≤ s.re\n          · rw [abs_of_nonneg hsign]\n            have h14 : (1.75 : ℝ) * 2 ≤ s.re := by linarith [hre2]\n            linarith [h14, hR]\n          · push Not at hsign\n            rw [abs_of_neg hsign]\n            linarith [h12]\n        have h14 : (100 : ℝ) / R < 1 := by\n          rw [div_lt_one hRpos]\n          linarith [hR]\n        rw [hre]\n        have h15 : s.re < 0 := by\n          by_cases hsign : 0 ≤ s.re\n          · have h16 : (1.75 : ℝ) * 2 ≤ s.re := by linarith [hre2]\n            linarith [h16, hR, h14]\n          · exact lt_of_not_ge hsign\n        linarith [h10, h14, hsign, h15]\n      -- the distance bound\n      have hdist : ∀ m : ℕ, (1 / 8 : ℝ) ≤ ‖(s / 2) + (m : ℂ)‖ := by\n        intro m\n        have h1 : ‖(s / 2) + (m : ℂ)‖ ≥ |((s / 2) + (m : ℂ)).re| := Complex.abs_re_le_norm _\n        have h2 : ((s / 2) + (m : ℂ)).re = s.re / 2 + (m : ℝ) := by\n          rw [Complex.add_re, hre, Complex.natCast_re]\n        rw [h2] at h1\n        -- (re s)/2 + R/2 ∈ [0, 50/R)\n        have hge : (0 : ℝ) ≤ s.re / 2 + R / 2 := by\n          have h9 : |s.re| ≤ R := by\n            have h10 := abs_re_le_norm s\n            rw [hs] at h10\n            exact h10\n          have h11 : -R ≤ s.re := by\n            have h12 := abs_le.mp (show |s.re| ≤ R from h9)\n            linarith [h12.1]\n          linarith [h11]\n        have hlt : s.re / 2 + R / 2 < 50 / R := by\n          have h13 : |s.re| > R - 100 / R := by\n            by_cases hsign : 0 ≤ s.re\n            · rw [abs_of_nonneg hsign]\n              have h14 : (1.75 : ℝ) * 2 ≤ s.re := by linarith [hre2]\n              linarith [h14, hR]\n            · push Not at hsign\n              rw [abs_of_neg hsign]\n              have h15 : s.re / 2 < 0 := hre_neg\n              linarith [h15, hRmin]\n          have h14 : s.re < 0 := hre_neg\n          linarith [h13, h14]\n        -- |x + m| ≥ |m − R/2| − (x + R/2) ≥ 1/4 − 50/R ≥ 1/8\n        have hgap' := hgapInt (m : ℤ)\n        have hcast : ((m : ℤ) : ℝ) = (m : ℝ) := by push_cast; ring\n        rw [hcast] at hgap'\n        have h4 : |s.re / 2 + (m : ℝ)| ≥ |(m : ℝ) - R / 2| - (s.re / 2 + R / 2) := by\n          have h5 : s.re / 2 + (m : ℝ) = ((m : ℝ) - R / 2) + (s.re / 2 + R / 2) := by ring\n          rw [h5]\n          have h6 : |(m : ℝ) - R / 2| ≤ |(m : ℝ) - R / 2 + (s.re / 2 + R / 2)|\n              + |s.re / 2 + R / 2| := by\n            have h7 := abs_add_le ((m : ℝ) - R / 2) (s.re / 2 + R / 2)\n            rw [show (m : ℝ) - R / 2 + (s.re / 2 + R / 2)\n                = (m : ℝ) - R / 2 + (s.re / 2 + R / 2) from rfl] at h7\n            have h8 : ((m : ℝ) - R / 2) = ((m : ℝ) - R / 2 + (s.re / 2 + R / 2))\n                - (s.re / 2 + R / 2) := by ring\n            rw [h8]\n            exact abs_sub_abs_le_abs_sub _ _\n          linarith [h6]\n        have h50 : (50 : ℝ) / R ≤ 1 / 8 := by\n          rw [div_le_iff₀ hRpos]\n          linarith [hR]\n        have h9 : |R / 2 - (m : ℝ)| = |(m : ℝ) - R / 2| := abs_sub_comm _ _\n        linarith [h1, h4, hgap', h9, hge, hlt, h50]\n      have hwre2 : (s / 2).re ≤ 2 := by linarith [hre_neg]\n      have h1 := norm_digamma_le_of_dist_nat (show (0 : ℝ) < 1 / 8 by norm_num)\n        hwre2 hdist\n      have h2 : (46 : ℝ) + 2 / (1 / 8) = 62 := by norm_num\n      rw [h2, hsnorm] at h1\n      exact h1\n\n/-- ‖1/s‖ ≤ 1 on ‖s‖ = R ≥ 1. -/\nlemma norm_one_div_le_of_norm_eq {s : ℂ} {R : ℝ} (hs : ‖s‖ = R) (hR : (1 : ℝ) ≤ R) :\n    ‖(1 : ℂ) / s‖ ≤ 1 := by\n  rw [norm_div, norm_one, hs]\n  exact div_le_one_of_le₀ hR hR\n\n/-- ‖1/(s−1)‖ ≤ 1 on ‖s‖ = R ≥ 2 (‖s−1‖ ≥ R−1 ≥ 1). -/\nlemma norm_one_div_sub_one_le_of_norm_eq {s : ℂ} {R : ℝ} (hs : ‖s‖ = R)\n    (hR : (2 : ℝ) ≤ R) : ‖(1 : ℂ) / (s - 1)‖ ≤ 1 := by\n  have hnorm : (1 : ℝ) ≤ ‖s - 1‖ := by\n    have h := abs_norm_sub_norm_le s (1 : ℂ)\n    rw [hs, norm_one, abs_of_nonneg (by linarith [hR] : (0 : ℝ) ≤ R - 1)] at h\n    linarith [h, hR]\n  rw [norm_div, norm_one]\n  exact div_le_one_of_le₀ hnorm hnorm\n\n/-- log π ≤ 2 (π < 3.15 ≤ e²). -/\nlemma log_pi_le_two : Real.log Real.pi ≤ 2 := by\n  rw [show (2 : ℝ) = Real.log (Real.exp 2) by rw [Real.log_exp]]\n  apply Real.log_le_log Real.pi_pos\n  have h1 : Real.exp 2 = (Real.exp 1) ^ 2 := by\n    rw [← Real.exp_nat_mul]; norm_num\n  have h2 : (2.7 : ℝ) ≤ Real.exp 1 := by\n    have h := Real.exp_one_gt_d9; linarith\n  have h3 : (2.7 : ℝ) ^ 2 ≤ (Real.exp 1) ^ 2 :=\n    pow_le_pow_left₀ (by norm_num) h2 2\n  have h4 := Real.pi_lt_315\n  have h5 : Real.pi ≤ (2.7 : ℝ) ^ 2 := by\n    have h6 : (2.7 : ℝ) ^ 2 = 7.29 := by norm_num\n    linarith [h4, h6]\n  linarith [h1, h3, h5]\n\n/-- ‖(log π : ℂ)/2‖ ≤ 1. -/\nlemma norm_logPi_div_two_le : ‖(Real.log Real.pi : ℂ) / 2‖ ≤ 1 := by\n  have hpos : (0 : ℝ) < Real.log Real.pi :=\n    Real.log_pos (by linarith [Real.pi_gt_three] : (1 : ℝ) < Real.pi)\n  have hle := log_pi_le_two\n  rw [norm_div]\n  have h1 : ‖(Real.log Real.pi : ℂ)‖ = Real.log Real.pi := by\n    rw [show ((Real.log Real.pi : ℂ)) = ((Real.log Real.pi : ℝ) : ℂ) from rfl,\n      Complex.norm_real, Real.norm_eq_abs, abs_of_pos hpos]\n  rw [h1]\n  have h2 : ‖(2 : ℂ)‖ = 2 := by\n    rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n    norm_num\n  rw [h2]\n  linarith [hle]\n\nend NguyenRH1\n\nend"},"extra_content":null}]