← Session 36 — ii′-6-DL dog-leg + side bounds; Paper A review
thinking (644 chars)
The Edit tool call got rejected due to a formatting issue with my parameters (I accidentally used `_raw`). Let me redo the edit properly. Also, my draft was cut off mid-way through hpt — I need to complete the rest of the mid-horizontal theorem (hpt, hswap, hper, hsum, hΣbound, the final calc) and the neg theorem. Let me write the complete §4 edit now (finishing the truncated draft).
The remaining parts after htermcont:
- hpt: pointwise ‖Σ‖ ≤ Σ m·(1/√)
- hswap: ∫ of the RHS sum = Σ m·∫
- hper: per-ρ integral ≤ 2·log(148.5·C0hat)
- hsum: Σ m·∫ ≤ B0·Z2hat
- hΣbound: ∫‖Σ‖ ≤ B0·Z2hat
- the final calc
- the neg theorem
Let me write it all.
The edit was malformed (truncated draft). Writing the complete §4 properly now.
tool: Edit
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSideBounds.lean",
"old_string": " _ = 2 * T * (Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by ring\n _ \u2264 Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d) := hfinal\n\nend NguyenRH1",
"new_string": " _ = 2 * T * (Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by ring\n _ \u2264 Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d) := hfinal\n\n/-! ## 4. 6-c-iv: the mid-horizontal segment machine [\u22125/2, 3] -/\n\n/-- **The arcsinh FTC machine** (6-c-iv core): the direct antiderivative\nF(\u03c3) = log((\u03c3\u2212\u03b2) + \u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2)) of 1/\u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2) (Real.arcsinh does\nnot exist here): g(\u03c3) := (\u03c3\u2212\u03b2)+\u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2) > 0 (\u221ah > |\u03c3\u2212\u03b2|), and\ng\u2032 = 1 + (\u03c3\u2212\u03b2)/\u221ah = g/\u221ah, so (log g)\u2032 = 1/\u221ah exactly. -/\ntheorem integral_one_div_sqrt_sq_add_sq (\u03b2 \u03b4 : \u211d) (h\u03b4 : 0 < \u03b4) (a b : \u211d) :\n \u222b \u03c3 in a..b, 1 / Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) =\n Real.log ((b - \u03b2) + Real.sqrt ((b - \u03b2) ^ 2 + \u03b4 ^ 2)) -\n Real.log ((a - \u03b2) + Real.sqrt ((a - \u03b2) ^ 2 + \u03b4 ^ 2)) := by\n have hh : \u2200 \u03c3 : \u211d, (0 : \u211d) < (\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2 := fun \u03c3 =>\n add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos h\u03b4 2)\n have hgpos : \u2200 \u03c3 : \u211d, (0 : \u211d) < (\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) := by\n intro \u03c3\n have h1 : |(\u03c3 - \u03b2)| < Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) := by\n have h2 : (\u03c3 - \u03b2) ^ 2 < (\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2 := by nlinarith [h\u03b4]\n have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2\n rwa [Real.sqrt_sq_eq_abs] at h3\n have h4 : -(\u03c3 - \u03b2) \u2264 |(\u03c3 - \u03b2)| := neg_abs_le (\u03c3 - \u03b2)\n linarith [h1, h4]\n have hderiv : \u2200 \u03c3 : \u211d, HasDerivAt\n (fun \u03c3 => Real.log ((\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)))\n (1 / Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u03c3 := by\n intro \u03c3\n have hh\u03c3 := hh \u03c3\n have hsqrt0 : Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2260 0 := ne_of_gt (Real.sqrt_pos.mpr hh\u03c3)\n have hg0 : ((\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u2260 0 := (hgpos \u03c3).ne'\n have h1 : HasDerivAt (fun \u03c3 => \u03c3 - \u03b2) 1 \u03c3 := hasDerivAt_id.sub_const \u03b2\n have h2 : HasDerivAt (fun \u03c3 => (\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) (2 * (\u03c3 - \u03b2)) \u03c3 := by\n have h2a := (hasDerivAt_id.sub_const \u03b2).pow 2\n have h2b := h2a.add_const (\u03b4 ^ 2)\n convert h2b using 1\n ring\n have h4 : HasDerivAt (fun \u03c3 => Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))\n (2 * (\u03c3 - \u03b2) / (2 * Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))) \u03c3 :=\n h2.sqrt hh\u03c3.ne'\n have h5 : HasDerivAt (fun \u03c3 => (\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))\n (1 + 2 * (\u03c3 - \u03b2) / (2 * Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))) \u03c3 :=\n h1.add h4\n have h6 : HasDerivAt (fun \u03c3 => (\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))\n (((\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)) /\n Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u03c3 := by\n convert h5 using 1\n field_simp [hsqrt0]\n ring\n have h7 := h6.log hg0\n convert h7 using 1\n field_simp [hsqrt0, hg0]\n ring\n exact intervalIntegral.integral_eq_sub_of_hasDerivAt (fun \u03c3 _ => hderiv \u03c3)\n (by\n apply Continuous.intervalIntegrable\n apply Continuous.div continuous_const\n \u00b7 exact Real.continuous_sqrt.comp (by fun_prop :\n Continuous fun \u03c3 : \u211d => (\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)\n \u00b7 intro \u03c3\n exact ne_of_gt (Real.sqrt_pos.mpr (hh \u03c3)))\n\n/-- **The right endpoint estimate** F(3) \u2264 log(6+\u03b4): \u221a((3\u2212\u03b2)\u00b2+\u03b4\u00b2) \u2264\n(3\u2212\u03b2)+\u03b4 for 3\u2212\u03b2 > 0, so the argument is \u2264 2(3\u2212\u03b2)+\u03b4 \u2264 6+\u03b4 (0 \u2264 \u03b2). -/\ntheorem arcsinh_right_endpoint_le {\u03b2 \u03b4 : \u211d} (h\u03b20 : 0 < \u03b2) (h\u03b21 : \u03b2 < 1)\n (h\u03b4 : 0 < \u03b4) :\n Real.log ((3 - \u03b2) + Real.sqrt ((3 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u2264 Real.log (6 + \u03b4) := by\n have hx : (0 : \u211d) < 3 - \u03b2 := by linarith\n have hsqrt_le : Real.sqrt ((3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2264 (3 - \u03b2) + \u03b4 := by\n rw [Real.sqrt_le_iff]\n exact \u27e8by positivity, by nlinarith [h\u03b4, hx]\u27e9\n have h1 : (0 : \u211d) < (3 - \u03b2) + Real.sqrt ((3 - \u03b2) ^ 2 + \u03b4 ^ 2) := by\n have h2 := Real.sqrt_nonneg ((3 - \u03b2) ^ 2 + \u03b4 ^ 2)\n nlinarith\n have h3 : (3 - \u03b2) + Real.sqrt ((3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2264 6 + \u03b4 := by\n nlinarith [hsqrt_le, h\u03b20]\n exact Real.log_le_log h1 h3\n\n/-- **The left endpoint estimate** \u2212F(\u22125/2) \u2264 log(7+\u03b4) + 2\u00b7log(1/\u03b4):\nwith u := 5/2+\u03b2 \u2208 (5/2, 7/2), the argument \u2212u+\u221a(u\u00b2+\u03b4\u00b2) rationalizes to\n\u03b4\u00b2/(u+\u221a(u\u00b2+\u03b4\u00b2)) \u2265 \u03b4\u00b2/(7+\u03b4) > 0, so F(\u22125/2) \u2265 log(\u03b4\u00b2/(7+\u03b4)) =\n2\u00b7log \u03b4 \u2212 log(7+\u03b4). -/\ntheorem arcsinh_left_endpoint_le {\u03b2 \u03b4 : \u211d} (h\u03b20 : 0 < \u03b2) (h\u03b21 : \u03b2 < 1)\n (h\u03b4 : 0 < \u03b4) :\n -Real.log ((-5 / 2 - \u03b2) + Real.sqrt ((-5 / 2 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u2264\n Real.log (7 + \u03b4) + 2 * Real.log (1 / \u03b4) := by\n have hu : (0 : \u211d) < 5 / 2 + \u03b2 := by linarith\n have hsq : (-5 / 2 - \u03b2) ^ 2 = (5 / 2 + \u03b2) ^ 2 := by ring\n have hneg : (-5 / 2 : \u211d) - \u03b2 = -(5 / 2 + \u03b2) := by ring\n rw [hsq, hneg]\n set u := 5 / 2 + \u03b2 with hu_def\n have hu2 : u < 7 / 2 := by rw [hu_def]; linarith\n have hsqrt_pos : (0 : \u211d) < Real.sqrt (u ^ 2 + \u03b4 ^ 2) :=\n Real.sqrt_pos.mpr (add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos h\u03b4 2))\n have hg_pos : (0 : \u211d) < -u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) := by\n have h1 : u < Real.sqrt (u ^ 2 + \u03b4 ^ 2) := by\n have h2 : u ^ 2 < u ^ 2 + \u03b4 ^ 2 := by nlinarith [h\u03b4]\n have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2\n rwa [Real.sqrt_sq_eq_abs, abs_of_pos hu] at h3\n linarith\n -- the rationalization: \u2212u + \u221a = \u03b4\u00b2/(u + \u221a)\n have hrid : -u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) =\n \u03b4 ^ 2 / (u + Real.sqrt (u ^ 2 + \u03b4 ^ 2)) := by\n rw [div_eq_iff (ne_of_gt (by linarith [hsqrt_pos] :\n (0 : \u211d) < u + Real.sqrt (u ^ 2 + \u03b4 ^ 2)))]\n have hs : (Real.sqrt (u ^ 2 + \u03b4 ^ 2)) ^ 2 = u ^ 2 + \u03b4 ^ 2 :=\n Real.sq_sqrt (by positivity)\n nlinarith [hs]\n -- the denominator \u2264 7 + \u03b4\n have hden : u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) \u2264 7 + \u03b4 := by\n have h1 : Real.sqrt (u ^ 2 + \u03b4 ^ 2) \u2264 u + \u03b4 := by\n rw [Real.sqrt_le_iff]\n exact \u27e8by linarith [h\u03b4, hu.le], by nlinarith [h\u03b4, hu]\u27e9\n nlinarith [h1, hu2]\n -- \u03b4\u00b2/(7+\u03b4) \u2264 \u03b4\u00b2/(u+\u221a) = \u2212u+\u221a\n have hge : \u03b4 ^ 2 / (7 + \u03b4) \u2264 -u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) := by\n rw [hrid]\n have h2 : (0 : \u211d) < u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) := by linarith [hsqrt_pos]\n exact div_le_div_of_nonneg_left (sq_nonneg _) h2 hden\n -- log mono + algebra: F(\u22125/2) \u2265 log(\u03b4\u00b2/(7+\u03b4)) = 2\u00b7log \u03b4 \u2212 log(7+\u03b4)\n have hlog : Real.log (\u03b4 ^ 2 / (7 + \u03b4)) \u2264 Real.log (-u + Real.sqrt (u ^ 2 + \u03b4 ^ 2)) :=\n Real.log_le_log (by positivity) hge\n have hlogid : Real.log (\u03b4 ^ 2 / (7 + \u03b4)) = 2 * Real.log \u03b4 - Real.log (7 + \u03b4) := by\n rw [Real.log_div (pow_pos h\u03b4 2).ne' (by linarith [h\u03b4] : (7 : \u211d) + \u03b4 \u2260 0),\n Real.log_pow]\n ring\n have hlog1 : Real.log (1 / \u03b4) = -Real.log \u03b4 := by\n rw [Real.log_div one_ne_zero (ne_of_gt h\u03b4), Real.log_one, zero_sub]\n rw [hlogid] at hlog\n linarith [hlog, hlog1]\n\n/-- **The per-zero segment integral bound**: \u222b_{\u22125/2}^{3} d\u03c3/\u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2)\n\u2264 2\u00b7log(16.5/\u03b4) for 0 < \u03b2 < 1, 0 < \u03b4 \u2264 1 \u2014 the two endpoint estimates +\nlog((6+\u03b4)(7+\u03b4)) \u2264 log(16.5\u00b2) since (6+\u03b4)(7+\u03b4) \u2264 56 \u2264 272.25. -/\ntheorem per_zero_integral_le_two_log {\u03b2 \u03b4 : \u211d} (h\u03b20 : 0 < \u03b2) (h\u03b21 : \u03b2 < 1)\n (h\u03b4 : 0 < \u03b4) (h\u03b41 : \u03b4 \u2264 1) :\n \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), 1 / Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2264\n 2 * Real.log (16.5 / \u03b4) := by\n have hftc := integral_one_div_sqrt_sq_add_sq \u03b2 \u03b4 h\u03b4 (-5 / 2) 3\n have hr := arcsinh_right_endpoint_le h\u03b20 h\u03b21 h\u03b4\n have hl := arcsinh_left_endpoint_le h\u03b20 h\u03b21 h\u03b4\n have h1 : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), 1 / Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2264\n Real.log (6 + \u03b4) + Real.log (7 + \u03b4) + 2 * Real.log (1 / \u03b4) := by\n rw [hftc]\n linarith [hr, hl]\n -- the log-mono simplification: log(6+\u03b4) + log(7+\u03b4) \u2264 2\u00b7log 16.5\n have h2 : Real.log (6 + \u03b4) + Real.log (7 + \u03b4) \u2264 2 * Real.log 16.5 := by\n have h3 : Real.log (6 + \u03b4) + Real.log (7 + \u03b4) = Real.log ((6 + \u03b4) * (7 + \u03b4)) :=\n (Real.log_mul (by linarith [h\u03b4] : (6 : \u211d) + \u03b4 \u2260 0)\n (by linarith [h\u03b4] : (7 : \u211d) + \u03b4 \u2260 0)).symm\n have h4 : Real.log ((6 + \u03b4) * (7 + \u03b4)) \u2264 Real.log (16.5 * 16.5) :=\n Real.log_le_log (by positivity) (by nlinarith [h\u03b4, h\u03b41])\n have h5 : Real.log (16.5 * 16.5) = 2 * Real.log 16.5 := by\n rw [show (16.5 : \u211d) * 16.5 = 16.5 ^ 2 by ring, Real.log_pow]\n ring\n linarith [h3, h4, h5]\n have h6 : 2 * Real.log (16.5 / \u03b4) = 2 * Real.log 16.5 + 2 * Real.log (1 / \u03b4) := by\n have h7 : Real.log (1 / \u03b4) = -Real.log \u03b4 := by\n rw [Real.log_div one_ne_zero (ne_of_gt h\u03b4), Real.log_one, zero_sub]\n rw [Real.log_div (by norm_num) (ne_of_gt h\u03b4), h7]\n ring\n rw [h6]\n linarith [h1, h2]\n\n/-- **6-c-iv (mid-horizontal [\u22125/2, 3] at height +T)**: the segment bound\n\u2016H\u2016 \u2264 (e\u2074+1)\u00b7(2\u00b7Z\u2082(T)\u00b7log(148.5\u00b7\u0108\u2080(\u221an+2)) + 5.5\u00b7(10.5\u00b7log(T+2)+48)).\nKernel e\u2074+1 (the ii\u2032-4 shift lemma at s := w\u22121); logDeriv split by\nnorm_le_insert' into the near sum (per-zero arcsinh-FTC machine +\nintegral_finsetSum + the two-unit count \u2264 Z\u2082(T)) and the tight R-bound\n(capstone, constant in \u03c3). -/\ntheorem hIntegral_Jlag_mid_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n (hNLZ : NoLowZeros) {n : \u2115} (hn : 100000 \u2264 n) {T : \u211d}\n (hTwide : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 Real.sqrt (n : \u211d) - 1 < \u03c1.im \u2192\n \u03c1.im < Real.sqrt (n : \u211d) + 2 \u2192\n 1 / (9 * C0hat (Real.sqrt (n : \u211d) + 2)) \u2264 |\u03c1.im - T|)\n (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) (-5 / 2) 3 T\u2016 \u2264\n (Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by\n classical\n have hnR : (100000 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have h10T : (10 : \u211d) \u2264 T := by\n have h1 : (10 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n linarith\n have hT0 : (0 : \u211d) \u2264 T := by linarith\n have hn1 : 1 \u2264 n := by omega\n have hlen : (-5 / 2 : \u211d) \u2264 3 := by norm_num\n have hC0 : (0 : \u211d) < C0hat (Real.sqrt (n : \u211d) + 2) := by\n have h2 := two_le_C0hat (by nlinarith [Real.sqrt_nonneg (n : \u211d)] :\n (1 : \u211d) \u2264 Real.sqrt (n : \u211d) + 2)\n linarith\n have hB0nn : (0 : \u211d) \u2264 2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) := by\n have h1 : (1 : \u211d) \u2264 148.5 * C0hat (Real.sqrt (n : \u211d) + 2) := by nlinarith [hC0]\n have h3 := Real.log_nonneg h1\n linarith\n -- zero-freeness on the horizontal + the path continuity machines\n have hzne : \u2200 \u03c3 : \u211d, riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) \u2260 0 :=\n fun \u03c3 => zeta_ne_zero_horizontal hTwide hn1 hTn hTn1\n have hne1 : \u2200 \u03c3 : \u211d, ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) \u2260 1 := by\n intro \u03c3 h\n have him := congrArg Complex.im h\n simp at him\n linarith [h10T]\n have hpath : Continuous fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I) := by\n fun_prop\n have hLDc : Continuous fun \u03c3 : \u211d =>\n logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) := by\n rw [continuous_iff_continuousAt]\n intro \u03c3\n have hf : ContinuousAt (fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) \u03c3 :=\n hpath.continuousAt\n exact ContinuousAt.comp (g := logDeriv riemannZeta)\n (f := fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) (x := \u03c3)\n (continuousAt_logDeriv_zeta (hne1 \u03c3) (hzne \u03c3)) hf\n have hJcont : \u2200 \u03c3 : \u211d, ContinuousAt (Jlag n) ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) := by\n intro \u03c3\n have hA := (kFun_differentiableAt (n := n) (hne1 \u03c3)).continuousAt\n have hB := continuousAt_logDeriv_zeta (hne1 \u03c3) (hzne \u03c3)\n show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\n exact hA.mul hB.neg\n have hcontJ : Continuous fun \u03c3 : \u211d =>\n Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) := by\n rw [continuous_iff_continuousAt]\n intro \u03c3\n have hf : ContinuousAt (fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) \u03c3 :=\n hpath.continuousAt\n exact ContinuousAt.comp (g := Jlag n)\n (f := fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) (x := \u03c3) (hJcont \u03c3) hf\n have hcontG : Continuous fun \u03c3 : \u211d =>\n \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 := continuous_norm.comp hcontJ\n have hJintbl : IntervalIntegrable\n (fun \u03c3 : \u211d => \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016)\n MeasureTheory.volume (-5 / 2) 3 := hcontG.intervalIntegrable _ _\n have hLDcont : Continuous fun \u03c3 : \u211d =>\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 :=\n continuous_norm.comp hLDc\n have hLDintbl : IntervalIntegrable\n (fun \u03c3 : \u211d => \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016)\n MeasureTheory.volume (-5 / 2) 3 := hLDcont.intervalIntegrable _ _\n have hKLcont : Continuous fun \u03c3 : \u211d =>\n (Real.exp 4 + 1) * \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 :=\n continuous_const.mul hLDcont\n have hKLintbl : IntervalIntegrable\n (fun \u03c3 : \u211d => (Real.exp 4 + 1) *\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016)\n MeasureTheory.volume (-5 / 2) 3 := hKLcont.intervalIntegrable _ _\n -- the near-sum denominator never vanishes on the path (else s = \u03c1 is a\n -- zero, contra zeta_ne_zero_horizontal)\n have hden : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u03c1 \u2208 nearZerosSub T \u2192\n \u2200 \u03c3 : \u211d, ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1 \u2260 0 := by\n intro \u03c1 _ \u03c3 h0\n have hs : ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) = \u03c1.1 := sub_eq_zero.mp h0\n have hz := hzne \u03c3\n rw [hs] at hz\n exact hz \u03c1.2.1\n have h\u03a3cont : Continuous fun \u03c3 : \u211d =>\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1) := by\n apply continuous_finset_sum\n intro \u03c1 h\u03c1\n exact Continuous.div continuous_const (hpath.sub continuous_const) (hden \u03c1 h\u03c1)\n have h\u03a3norm_cont : Continuous fun \u03c3 : \u211d =>\n \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\n continuous_norm.comp h\u03a3cont\n have h\u03a3norm_int : IntervalIntegrable\n (fun \u03c3 : \u211d => \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016)\n MeasureTheory.volume (-5 / 2) 3 := h\u03a3norm_cont.intervalIntegrable _ _\n have hRcont : Continuous fun \u03c3 : \u211d =>\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\n continuous_norm.comp (hLDc.sub h\u03a3cont)\n have hRnorm_int : IntervalIntegrable\n (fun \u03c3 : \u211d => \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016)\n MeasureTheory.volume (-5 / 2) 3 := hRcont.intervalIntegrable _ _\n -- the per-\u03c1 data (\u03b4_\u03c1 := |\u03b3\u2212T| \u2208 [c_clear, 1))\n have h\u03c1data : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u03c1 \u2208 nearZerosSub T \u2192\n (0 : \u211d) < |\u03c1.1.im - T| \u2227 |\u03c1.1.im - T| < 1 \u2227\n (1 / (9 * C0hat (Real.sqrt (n : \u211d) + 2))) \u2264 |\u03c1.1.im - T| := by\n intro \u03c1 h\u03c1\n have h\u03b41 := mem_nearZerosSub.mp h\u03c1\n obtain \u27e8hlo, hhi\u27e9 := abs_lt.mp h\u03b41\n have h\u03b31 : Real.sqrt (n : \u211d) - 1 < \u03c1.1.im := by nlinarith [hTn]\n have h\u03b32 : \u03c1.1.im < Real.sqrt (n : \u211d) + 2 := by nlinarith [hTn1]\n have h\u03b4ge := hTwide \u03c1.1 \u03c1.2 h\u03b31 h\u03b32\n have h\u03b4pos : (0 : \u211d) < |\u03c1.1.im - T| :=\n lt_of_lt_of_le (one_div_pos.mpr (by positivity :\n (0 : \u211d) < 9 * C0hat (Real.sqrt (n : \u211d) + 2))) h\u03b4ge\n exact \u27e8h\u03b4pos, h\u03b41, h\u03b4ge\u27e9\n -- the kernel bound per \u03c3 (the ii\u2032-4 shift lemma at s := w \u2212 1)\n have hnT2 : (n : \u211d) \u2264 T ^ 2 := by\n have h1 : (Real.sqrt (n : \u211d)) ^ 2 \u2264 T ^ 2 :=\n pow_le_pow_left\u2080 (Real.sqrt_nonneg _) hTn 2\n rwa [Real.sq_sqrt (by positivity : (0 : \u211d) \u2264 (n : \u211d))] at h1\n have hker : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\n \u2016kFun n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264 Real.exp 4 + 1 := by\n intro \u03c3 h\u03c3\n obtain \u27e8h\u03c31, h\u03c32\u27e9 := h\u03c3\n have hre : (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - 1).re = \u03c3 - 1 := by simp\n have him : (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - 1).im = T := by simp\n have h1 := kFun_shift_norm_le_exp_four_add_one (n := n)\n (s := (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - 1))\n (by rw [hre]; linarith [h\u03c32]) (by rw [him]; exact hnT2)\n rwa [sub_add_cancel] at h1\n -- pointwise Jlag \u2264 (e\u2074+1)\u00b7\u2016logDeriv\u2016\n have hptJ : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\n \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264\n (Real.exp 4 + 1) * \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 := by\n intro \u03c3 h\u03c3\n rw [Jlag_norm_eq]\n exact mul_le_mul (hker \u03c3 h\u03c3) le_rfl (norm_nonneg _) (by positivity)\n have hJint : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264\n (Real.exp 4 + 1) * \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 := by\n have h := intervalIntegral.integral_mono_on hlen hJintbl hKLintbl\n (fun \u03c3 h\u03c3 => hptJ \u03c3 h\u03c3)\n rwa [intervalIntegral.integral_const_mul] at h\n -- the logDeriv split: \u2016logDeriv\u2016 \u2264 \u2016\u03a3\u2016 + \u2016logDeriv \u2212 \u03a3\u2016\n have hsumcont : Continuous fun \u03c3 : \u211d =>\n \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 +\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\n h\u03a3norm_cont.add hRcont\n have hsum_intbl : IntervalIntegrable\n (fun \u03c3 : \u211d => \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 +\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016)\n MeasureTheory.volume (-5 / 2) 3 := hsumcont.intervalIntegrable _ _\n have hsplit : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016) +\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016) := by\n have hpt2 : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264\n \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 +\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\n fun \u03c3 _ => norm_le_insert' _ _\n have h := intervalIntegral.integral_mono_on hlen hLDintbl hsum_intbl\n (fun \u03c3 h\u03c3 => hpt2 \u03c3 h\u03c3)\n rwa [intervalIntegral.integral_add h\u03a3norm_int hRnorm_int] at h\n -- the R-part integral (the 5f capstone, constant in \u03c3)\n have hR : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 \u2264\n 10.5 * Real.log (T + 2) + 48 := by\n intro \u03c3 h\u03c3\n obtain \u27e8h\u03c31, h\u03c32\u27e9 := h\u03c3\n have hre : ((\u03c3 : \u211d) + (T : \u211d) * Complex.I).re = \u03c3 := by simp\n have him : ((\u03c3 : \u211d) + (T : \u211d) * Complex.I).im = T := by simp\n have h := logDeriv_riemannZeta_sub_nearZeros_le_tight (t := T)\n (s := ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)) hZC hZC2 hNLZ h10T\n (by rw [hre]; exact h\u03c31) (by rw [hre]; exact h\u03c32) him (hzne \u03c3)\n rwa [abs_of_nonneg hT0] at h\n have hRint : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 \u2264\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48) := by\n have h := intervalIntegral.integral_mono_on hlen hRnorm_int intervalIntegrable_const\n (fun \u03c3 h\u03c3 => hR \u03c3 h\u03c3)\n rwa [intervalIntegral.integral_const, smul_eq_mul] at h\n -- the near-sum integral: the per-zero arcsinh-FTC machine + the swap\n have hnormid : \u2200 \u03c3 : \u211d, \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n \u2016((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1\u2016 =\n Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2) := by\n intro \u03c3 \u03c1\n have h1 : Complex.normSq (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1) =\n (\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n symm\n rw [Real.sqrt_eq_iff_eq_sq (by positivity) (norm_nonneg _),\n \u2190 Complex.normSq_eq_norm_sq]\n exact h1.symm\n have htermcont : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u03c1 \u2208 nearZerosSub T \u2192\n Continuous fun \u03c3 : \u211d => (zeroMult \u03c1.1 : \u211d) *\n (1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) := by\n intro \u03c1 h\u03c1\n obtain \u27e8h\u03b4pos, -, -\u27e9 := h\u03c1data \u03c1 h\u03c1\n have hh : \u2200 \u03c3 : \u211d, (0 : \u211d) < (\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2 := by\n intro \u03c3\n have h3 : \u03c1.1.im - T \u2260 0 := abs_pos.mp h\u03b4pos\n have h4 : T - \u03c1.1.im \u2260 0 := by\n intro h5\n apply h3\n linarith [h5]\n exact add_pos_of_nonneg_of_pos (sq_nonneg _) (sq_pos_of_ne_zero h4)\n apply Continuous.mul continuous_const\n apply Continuous.div continuous_const\n \u00b7 exact Real.continuous_sqrt.comp (by fun_prop :\n Continuous fun \u03c3 : \u211d => (\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)\n \u00b7 intro \u03c3\n exact ne_of_gt (Real.sqrt_pos.mpr (hh \u03c3))\n -- pointwise: \u2016\u03a3\u2016 \u2264 \u03a3 mult\u00b7(1/\u221a)\n have hpt : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\n \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 \u2264\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) := by\n intro \u03c3 _\n calc \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016\n \u2264 \u2211 \u03c1 \u2208 nearZerosSub T, \u2016(zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\n norm_sum_le _ _\n _ = \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) /\n \u2016((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1\u2016 := by\n apply Finset.sum_congr rfl\n intro \u03c1 _\n rw [norm_div]\n have h2 : \u2016(zeroMult \u03c1.1 : \u2102)\u2016 = (zeroMult \u03c1.1 : \u211d) := by\n rw [show (zeroMult \u03c1.1 : \u2102) = ((zeroMult \u03c1.1 : \u211d) : \u2102) by\n push_cast; ring, Complex.norm_real]\n exact abs_of_nonneg (Nat.cast_nonneg _)\n rw [h2]\n _ = \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) := by\n apply Finset.sum_congr rfl\n intro \u03c1 _\n rw [hnormid \u03c3 \u03c1, mul_one_div]\n -- the swap \u222b\u03a3 = \u03a3\u222b\n have hswap : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n (\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2))) =\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n 1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) := by\n rw [intervalIntegral.integral_finsetSum\n (fun \u03c1 h\u03c1 => (htermcont \u03c1 h\u03c1).intervalIntegrable _ _)]\n apply Finset.sum_congr rfl\n intro \u03c1 _\n exact intervalIntegral.integral_const_mul _ _\n -- per-\u03c1: the integral \u2264 2\u00b7log(148.5\u00b7\u0108\u2080(\u221an+2))\n have hper : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u03c1 \u2208 nearZerosSub T \u2192\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n 1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) \u2264\n 2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) := by\n intro \u03c1 h\u03c1\n obtain \u27e8h\u03b4pos, h\u03b41, h\u03b4ge\u27e9 := h\u03c1data \u03c1 h\u03c1\n have hsq : (T - \u03c1.1.im) ^ 2 = |\u03c1.1.im - T| ^ 2 := by\n rw [\u2190 sq_abs (\u03c1.1.im - T)]\n ring\n have hmain := per_zero_integral_le_two_log \u03c1.2.2.1 \u03c1.2.2.2 h\u03b4pos h\u03b41.le\n rw [hsq] at hmain \u22a2\n have hinv : 1 / |\u03c1.1.im - T| \u2264 9 * C0hat (Real.sqrt (n : \u211d) + 2) := by\n have h := one_div_le_one_div_of_le (one_div_pos.mpr (by positivity :\n (0 : \u211d) < 9 * C0hat (Real.sqrt (n : \u211d) + 2))) h\u03b4ge\n rwa [one_div_one_div] at h\n have h1 : (16.5 : \u211d) * (1 / |\u03c1.1.im - T|) \u2264\n 16.5 * (9 * C0hat (Real.sqrt (n : \u211d) + 2)) :=\n mul_le_mul_of_nonneg_left hinv (by norm_num)\n have h2 : (16.5 : \u211d) / |\u03c1.1.im - T| \u2264 148.5 * C0hat (Real.sqrt (n : \u211d) + 2) := by\n rw [mul_one_div, show (16.5 : \u211d) * (9 * C0hat (Real.sqrt (n : \u211d) + 2)) =\n 148.5 * C0hat (Real.sqrt (n : \u211d) + 2) by ring] at h1\n exact h1\n have h3 : Real.log (16.5 / |\u03c1.1.im - T|) \u2264\n Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) :=\n Real.log_le_log (by positivity) h2\n linarith [hmain, h3]\n -- the sum bound: \u03a3 mult\u00b7\u222b \u2264 (2\u00b7log(148.5\u00b7\u0108\u2080))\u00b7Z\u2082(T)\n have hsum : \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n 1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) \u2264\n (2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2))) * Z2hat T := by\n calc \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n 1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2))\n \u2264 \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2))) := by\n apply Finset.sum_le_sum\n intro \u03c1 h\u03c1\n exact mul_le_mul_of_nonneg_left (hper \u03c1 h\u03c1) (Nat.cast_nonneg _)\n _ = (2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2))) *\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) := by\n rw [\u2190 Finset.mul_sum]\n apply Finset.sum_congr rfl\n intro \u03c1 _\n ring\n _ \u2264 (2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2))) * Z2hat T :=\n mul_le_mul_of_nonneg_left (nearZerosSub_mult_sum_le hZC2 h10T) hB0nn\n -- the near-sum integral bound\n have hRHScont : Continuous fun \u03c3 : \u211d =>\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) := by\n apply continuous_finset_sum\n intro \u03c1 h\u03c1\n exact htermcont \u03c1 h\u03c1\n have h\u03a3bound : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 \u2264\n (2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2))) * Z2hat T := by\n have h1 : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 \u2264\n \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n (\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2))) :=\n intervalIntegral.integral_mono_on hlen h\u03a3norm_int\n (hRHScont.intervalIntegrable _ _) (fun \u03c3 h\u03c3 => hpt \u03c3 h\u03c3)\n exact h1.trans (hswap.trans_le hsum)\n -- assembly\n unfold HIntegral\n calc \u2016\u222b x in (-5 / 2 : \u211d)..(3 : \u211d), Jlag n ((x : \u211d) + (T : \u211d) * Complex.I)\u2016\n \u2264 \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 :=\n intervalIntegral.norm_integral_le_integral_norm hlen\n _ \u2264 (Real.exp 4 + 1) * \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 := hJint\n _ \u2264 (Real.exp 4 + 1) *\n ((\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016) +\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016)) :=\n mul_le_mul_of_nonneg_left hsplit (by positivity)\n _ \u2264 (Real.exp 4 + 1) *\n ((2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2))) * Z2hat T +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) :=\n mul_le_mul_of_nonneg_left (add_le_add h\u03a3bound hRint) (by positivity)\n _ = (Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by ring\n\n/-- **6-c-iv (the bottom side \u2212T)**: the conj trick (DL-5 pattern). -/\ntheorem hIntegral_Jlag_mid_neg_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n (hNLZ : NoLowZeros) {n : \u2115} (hn : 100000 \u2264 n) {T : \u211d}\n (hTwide : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 Real.sqrt (n : \u211d) - 1 < \u03c1.im \u2192\n \u03c1.im < Real.sqrt (n : \u211d) + 2 \u2192\n 1 / (9 * C0hat (Real.sqrt (n : \u211d) + 2)) \u2264 |\u03c1.im - T|)\n (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) (-5 / 2) 3 (-T)\u2016 \u2264\n (Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by\n have hnR : (100000 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hT0 : (0 : \u211d) < T := by\n have h1 : (0 : \u211d) < Real.sqrt (n : \u211d) := Real.sqrt_pos.mpr (by linarith)\n linarith\n have hconj : HIntegral (Jlag n) (-5 / 2) 3 (-T) =\n (starRingEnd \u2102) (HIntegral (Jlag n) (-5 / 2) 3 T) := by\n unfold HIntegral\n rw [\u2190 intervalIntegral.intervalIntegral_conj]\n apply intervalIntegral.integral_congr\n intro \u03c3 h\u03c3\n show Jlag n ((\u03c3 : \u211d) + (((-T : \u211d)) : \u2102) * Complex.I) =\n (starRingEnd \u2102) (Jlag n ((\u03c3 : \u211d) + T * Complex.I))\n have hid2 : ((\u03c3 : \u211d) + (((-T : \u211d)) : \u2102) * Complex.I) =\n (starRingEnd \u2102) ((\u03c3 : \u211d) + T * Complex.I) := by simp\n rw [hid2]\n exact Jlag_conj n (by\n intro h\n have him : (((\u03c3 : \u211d) + T * Complex.I)).im = T := by simp\n rw [h] at him\n simp at him\n linarith [hT0])\n rw [hconj, Complex.norm_conj]\n exact hIntegral_Jlag_mid_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1\n\nend NguyenRH1"
}
raw content_json (database row)
[{"type":"thinking","thinking":"The Edit tool call got rejected due to a formatting issue with my parameters (I accidentally used `_raw`). Let me redo the edit properly. Also, my draft was cut off mid-way through hpt — I need to complete the rest of the mid-horizontal theorem (hpt, hswap, hper, hsum, hΣbound, the final calc) and the neg theorem. Let me write the complete §4 edit now (finishing the truncated draft).\n\nThe remaining parts after htermcont:\n- hpt: pointwise ‖Σ‖ ≤ Σ m·(1/√)\n- hswap: ∫ of the RHS sum = Σ m·∫\n- hper: per-ρ integral ≤ 2·log(148.5·C0hat)\n- hsum: Σ m·∫ ≤ B0·Z2hat\n- hΣbound: ∫‖Σ‖ ≤ B0·Z2hat\n- the final calc\n- the neg theorem\n\nLet me write it all.","signature":""},{"type":"text","text":"The edit was malformed (truncated draft). Writing the complete §4 properly now."},{"type":"tool_use","id":"Edit_96","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSideBounds.lean","old_string":" _ = 2 * T * (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by ring\n _ ≤ Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := hfinal\n\nend NguyenRH1","new_string":" _ = 2 * T * (Real.exp (Real.sqrt (n : ℝ) / 2 + 1 / 3) + 1) *\n ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by ring\n _ ≤ Real.exp (1 / 3 : ℝ) * IIMaj (n : ℝ) := hfinal\n\n/-! ## 4. 6-c-iv: the mid-horizontal segment machine [−5/2, 3] -/\n\n/-- **The arcsinh FTC machine** (6-c-iv core): the direct antiderivative\nF(σ) = log((σ−β) + √((σ−β)²+δ²)) of 1/√((σ−β)²+δ²) (Real.arcsinh does\nnot exist here): g(σ) := (σ−β)+√((σ−β)²+δ²) > 0 (√h > |σ−β|), and\ng′ = 1 + (σ−β)/√h = g/√h, so (log g)′ = 1/√h exactly. -/\ntheorem integral_one_div_sqrt_sq_add_sq (β δ : ℝ) (hδ : 0 < δ) (a b : ℝ) :\n ∫ σ in a..b, 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) =\n Real.log ((b - β) + Real.sqrt ((b - β) ^ 2 + δ ^ 2)) -\n Real.log ((a - β) + Real.sqrt ((a - β) ^ 2 + δ ^ 2)) := by\n have hh : ∀ σ : ℝ, (0 : ℝ) < (σ - β) ^ 2 + δ ^ 2 := fun σ =>\n add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos hδ 2)\n have hgpos : ∀ σ : ℝ, (0 : ℝ) < (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by\n intro σ\n have h1 : |(σ - β)| < Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by\n have h2 : (σ - β) ^ 2 < (σ - β) ^ 2 + δ ^ 2 := by nlinarith [hδ]\n have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2\n rwa [Real.sqrt_sq_eq_abs] at h3\n have h4 : -(σ - β) ≤ |(σ - β)| := neg_abs_le (σ - β)\n linarith [h1, h4]\n have hderiv : ∀ σ : ℝ, HasDerivAt\n (fun σ => Real.log ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)))\n (1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) σ := by\n intro σ\n have hhσ := hh σ\n have hsqrt0 : Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hhσ)\n have hg0 : ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) ≠ 0 := (hgpos σ).ne'\n have h1 : HasDerivAt (fun σ => σ - β) 1 σ := hasDerivAt_id.sub_const β\n have h2 : HasDerivAt (fun σ => (σ - β) ^ 2 + δ ^ 2) (2 * (σ - β)) σ := by\n have h2a := (hasDerivAt_id.sub_const β).pow 2\n have h2b := h2a.add_const (δ ^ 2)\n convert h2b using 1\n ring\n have h4 : HasDerivAt (fun σ => Real.sqrt ((σ - β) ^ 2 + δ ^ 2))\n (2 * (σ - β) / (2 * Real.sqrt ((σ - β) ^ 2 + δ ^ 2))) σ :=\n h2.sqrt hhσ.ne'\n have h5 : HasDerivAt (fun σ => (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2))\n (1 + 2 * (σ - β) / (2 * Real.sqrt ((σ - β) ^ 2 + δ ^ 2))) σ :=\n h1.add h4\n have h6 : HasDerivAt (fun σ => (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2))\n (((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) /\n Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) σ := by\n convert h5 using 1\n field_simp [hsqrt0]\n ring\n have h7 := h6.log hg0\n convert h7 using 1\n field_simp [hsqrt0, hg0]\n ring\n exact intervalIntegral.integral_eq_sub_of_hasDerivAt (fun σ _ => hderiv σ)\n (by\n apply Continuous.intervalIntegrable\n apply Continuous.div continuous_const\n · exact Real.continuous_sqrt.comp (by fun_prop :\n Continuous fun σ : ℝ => (σ - β) ^ 2 + δ ^ 2)\n · intro σ\n exact ne_of_gt (Real.sqrt_pos.mpr (hh σ)))\n\n/-- **The right endpoint estimate** F(3) ≤ log(6+δ): √((3−β)²+δ²) ≤\n(3−β)+δ for 3−β > 0, so the argument is ≤ 2(3−β)+δ ≤ 6+δ (0 ≤ β). -/\ntheorem arcsinh_right_endpoint_le {β δ : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)\n (hδ : 0 < δ) :\n Real.log ((3 - β) + Real.sqrt ((3 - β) ^ 2 + δ ^ 2)) ≤ Real.log (6 + δ) := by\n have hx : (0 : ℝ) < 3 - β := by linarith\n have hsqrt_le : Real.sqrt ((3 - β) ^ 2 + δ ^ 2) ≤ (3 - β) + δ := by\n rw [Real.sqrt_le_iff]\n exact ⟨by positivity, by nlinarith [hδ, hx]⟩\n have h1 : (0 : ℝ) < (3 - β) + Real.sqrt ((3 - β) ^ 2 + δ ^ 2) := by\n have h2 := Real.sqrt_nonneg ((3 - β) ^ 2 + δ ^ 2)\n nlinarith\n have h3 : (3 - β) + Real.sqrt ((3 - β) ^ 2 + δ ^ 2) ≤ 6 + δ := by\n nlinarith [hsqrt_le, hβ0]\n exact Real.log_le_log h1 h3\n\n/-- **The left endpoint estimate** −F(−5/2) ≤ log(7+δ) + 2·log(1/δ):\nwith u := 5/2+β ∈ (5/2, 7/2), the argument −u+√(u²+δ²) rationalizes to\nδ²/(u+√(u²+δ²)) ≥ δ²/(7+δ) > 0, so F(−5/2) ≥ log(δ²/(7+δ)) =\n2·log δ − log(7+δ). -/\ntheorem arcsinh_left_endpoint_le {β δ : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)\n (hδ : 0 < δ) :\n -Real.log ((-5 / 2 - β) + Real.sqrt ((-5 / 2 - β) ^ 2 + δ ^ 2)) ≤\n Real.log (7 + δ) + 2 * Real.log (1 / δ) := by\n have hu : (0 : ℝ) < 5 / 2 + β := by linarith\n have hsq : (-5 / 2 - β) ^ 2 = (5 / 2 + β) ^ 2 := by ring\n have hneg : (-5 / 2 : ℝ) - β = -(5 / 2 + β) := by ring\n rw [hsq, hneg]\n set u := 5 / 2 + β with hu_def\n have hu2 : u < 7 / 2 := by rw [hu_def]; linarith\n have hsqrt_pos : (0 : ℝ) < Real.sqrt (u ^ 2 + δ ^ 2) :=\n Real.sqrt_pos.mpr (add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos hδ 2))\n have hg_pos : (0 : ℝ) < -u + Real.sqrt (u ^ 2 + δ ^ 2) := by\n have h1 : u < Real.sqrt (u ^ 2 + δ ^ 2) := by\n have h2 : u ^ 2 < u ^ 2 + δ ^ 2 := by nlinarith [hδ]\n have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2\n rwa [Real.sqrt_sq_eq_abs, abs_of_pos hu] at h3\n linarith\n -- the rationalization: −u + √ = δ²/(u + √)\n have hrid : -u + Real.sqrt (u ^ 2 + δ ^ 2) =\n δ ^ 2 / (u + Real.sqrt (u ^ 2 + δ ^ 2)) := by\n rw [div_eq_iff (ne_of_gt (by linarith [hsqrt_pos] :\n (0 : ℝ) < u + Real.sqrt (u ^ 2 + δ ^ 2)))]\n have hs : (Real.sqrt (u ^ 2 + δ ^ 2)) ^ 2 = u ^ 2 + δ ^ 2 :=\n Real.sq_sqrt (by positivity)\n nlinarith [hs]\n -- the denominator ≤ 7 + δ\n have hden : u + Real.sqrt (u ^ 2 + δ ^ 2) ≤ 7 + δ := by\n have h1 : Real.sqrt (u ^ 2 + δ ^ 2) ≤ u + δ := by\n rw [Real.sqrt_le_iff]\n exact ⟨by linarith [hδ, hu.le], by nlinarith [hδ, hu]⟩\n nlinarith [h1, hu2]\n -- δ²/(7+δ) ≤ δ²/(u+√) = −u+√\n have hge : δ ^ 2 / (7 + δ) ≤ -u + Real.sqrt (u ^ 2 + δ ^ 2) := by\n rw [hrid]\n have h2 : (0 : ℝ) < u + Real.sqrt (u ^ 2 + δ ^ 2) := by linarith [hsqrt_pos]\n exact div_le_div_of_nonneg_left (sq_nonneg _) h2 hden\n -- log mono + algebra: F(−5/2) ≥ log(δ²/(7+δ)) = 2·log δ − log(7+δ)\n have hlog : Real.log (δ ^ 2 / (7 + δ)) ≤ Real.log (-u + Real.sqrt (u ^ 2 + δ ^ 2)) :=\n Real.log_le_log (by positivity) hge\n have hlogid : Real.log (δ ^ 2 / (7 + δ)) = 2 * Real.log δ - Real.log (7 + δ) := by\n rw [Real.log_div (pow_pos hδ 2).ne' (by linarith [hδ] : (7 : ℝ) + δ ≠ 0),\n Real.log_pow]\n ring\n have hlog1 : Real.log (1 / δ) = -Real.log δ := by\n rw [Real.log_div one_ne_zero (ne_of_gt hδ), Real.log_one, zero_sub]\n rw [hlogid] at hlog\n linarith [hlog, hlog1]\n\n/-- **The per-zero segment integral bound**: ∫_{−5/2}^{3} dσ/√((σ−β)²+δ²)\n≤ 2·log(16.5/δ) for 0 < β < 1, 0 < δ ≤ 1 — the two endpoint estimates +\nlog((6+δ)(7+δ)) ≤ log(16.5²) since (6+δ)(7+δ) ≤ 56 ≤ 272.25. -/\ntheorem per_zero_integral_le_two_log {β δ : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)\n (hδ : 0 < δ) (hδ1 : δ ≤ 1) :\n ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≤\n 2 * Real.log (16.5 / δ) := by\n have hftc := integral_one_div_sqrt_sq_add_sq β δ hδ (-5 / 2) 3\n have hr := arcsinh_right_endpoint_le hβ0 hβ1 hδ\n have hl := arcsinh_left_endpoint_le hβ0 hβ1 hδ\n have h1 : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≤\n Real.log (6 + δ) + Real.log (7 + δ) + 2 * Real.log (1 / δ) := by\n rw [hftc]\n linarith [hr, hl]\n -- the log-mono simplification: log(6+δ) + log(7+δ) ≤ 2·log 16.5\n have h2 : Real.log (6 + δ) + Real.log (7 + δ) ≤ 2 * Real.log 16.5 := by\n have h3 : Real.log (6 + δ) + Real.log (7 + δ) = Real.log ((6 + δ) * (7 + δ)) :=\n (Real.log_mul (by linarith [hδ] : (6 : ℝ) + δ ≠ 0)\n (by linarith [hδ] : (7 : ℝ) + δ ≠ 0)).symm\n have h4 : Real.log ((6 + δ) * (7 + δ)) ≤ Real.log (16.5 * 16.5) :=\n Real.log_le_log (by positivity) (by nlinarith [hδ, hδ1])\n have h5 : Real.log (16.5 * 16.5) = 2 * Real.log 16.5 := by\n rw [show (16.5 : ℝ) * 16.5 = 16.5 ^ 2 by ring, Real.log_pow]\n ring\n linarith [h3, h4, h5]\n have h6 : 2 * Real.log (16.5 / δ) = 2 * Real.log 16.5 + 2 * Real.log (1 / δ) := by\n have h7 : Real.log (1 / δ) = -Real.log δ := by\n rw [Real.log_div one_ne_zero (ne_of_gt hδ), Real.log_one, zero_sub]\n rw [Real.log_div (by norm_num) (ne_of_gt hδ), h7]\n ring\n rw [h6]\n linarith [h1, h2]\n\n/-- **6-c-iv (mid-horizontal [−5/2, 3] at height +T)**: the segment bound\n‖H‖ ≤ (e⁴+1)·(2·Z₂(T)·log(148.5·Ĉ₀(√n+2)) + 5.5·(10.5·log(T+2)+48)).\nKernel e⁴+1 (the ii′-4 shift lemma at s := w−1); logDeriv split by\nnorm_le_insert' into the near sum (per-zero arcsinh-FTC machine +\nintegral_finsetSum + the two-unit count ≤ Z₂(T)) and the tight R-bound\n(capstone, constant in σ). -/\ntheorem hIntegral_Jlag_mid_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n (hNLZ : NoLowZeros) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}\n (hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt (n : ℝ) - 1 < ρ.im →\n ρ.im < Real.sqrt (n : ℝ) + 2 →\n 1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤ |ρ.im - T|)\n (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n ‖HIntegral (Jlag n) (-5 / 2) 3 T‖ ≤\n (Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by\n classical\n have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n have h10T : (10 : ℝ) ≤ T := by\n have h1 : (10 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n linarith\n have hT0 : (0 : ℝ) ≤ T := by linarith\n have hn1 : 1 ≤ n := by omega\n have hlen : (-5 / 2 : ℝ) ≤ 3 := by norm_num\n have hC0 : (0 : ℝ) < C0hat (Real.sqrt (n : ℝ) + 2) := by\n have h2 := two_le_C0hat (by nlinarith [Real.sqrt_nonneg (n : ℝ)] :\n (1 : ℝ) ≤ Real.sqrt (n : ℝ) + 2)\n linarith\n have hB0nn : (0 : ℝ) ≤ 2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) := by\n have h1 : (1 : ℝ) ≤ 148.5 * C0hat (Real.sqrt (n : ℝ) + 2) := by nlinarith [hC0]\n have h3 := Real.log_nonneg h1\n linarith\n -- zero-freeness on the horizontal + the path continuity machines\n have hzne : ∀ σ : ℝ, riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 0 :=\n fun σ => zeta_ne_zero_horizontal hTwide hn1 hTn hTn1\n have hne1 : ∀ σ : ℝ, ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 1 := by\n intro σ h\n have him := congrArg Complex.im h\n simp at him\n linarith [h10T]\n have hpath : Continuous fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I) := by\n fun_prop\n have hLDc : Continuous fun σ : ℝ =>\n logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) := by\n rw [continuous_iff_continuousAt]\n intro σ\n have hf : ContinuousAt (fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) σ :=\n hpath.continuousAt\n exact ContinuousAt.comp (g := logDeriv riemannZeta)\n (f := fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) (x := σ)\n (continuousAt_logDeriv_zeta (hne1 σ) (hzne σ)) hf\n have hJcont : ∀ σ : ℝ, ContinuousAt (Jlag n) ((σ : ℝ) + (T : ℝ) * Complex.I) := by\n intro σ\n have hA := (kFun_differentiableAt (n := n) (hne1 σ)).continuousAt\n have hB := continuousAt_logDeriv_zeta (hne1 σ) (hzne σ)\n show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\n exact hA.mul hB.neg\n have hcontJ : Continuous fun σ : ℝ =>\n Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I) := by\n rw [continuous_iff_continuousAt]\n intro σ\n have hf : ContinuousAt (fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) σ :=\n hpath.continuousAt\n exact ContinuousAt.comp (g := Jlag n)\n (f := fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) (x := σ) (hJcont σ) hf\n have hcontG : Continuous fun σ : ℝ =>\n ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := continuous_norm.comp hcontJ\n have hJintbl : IntervalIntegrable\n (fun σ : ℝ => ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖)\n MeasureTheory.volume (-5 / 2) 3 := hcontG.intervalIntegrable _ _\n have hLDcont : Continuous fun σ : ℝ =>\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ :=\n continuous_norm.comp hLDc\n have hLDintbl : IntervalIntegrable\n (fun σ : ℝ => ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖)\n MeasureTheory.volume (-5 / 2) 3 := hLDcont.intervalIntegrable _ _\n have hKLcont : Continuous fun σ : ℝ =>\n (Real.exp 4 + 1) * ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ :=\n continuous_const.mul hLDcont\n have hKLintbl : IntervalIntegrable\n (fun σ : ℝ => (Real.exp 4 + 1) *\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖)\n MeasureTheory.volume (-5 / 2) 3 := hKLcont.intervalIntegrable _ _\n -- the near-sum denominator never vanishes on the path (else s = ρ is a\n -- zero, contra zeta_ne_zero_horizontal)\n have hden : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →\n ∀ σ : ℝ, ((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1 ≠ 0 := by\n intro ρ _ σ h0\n have hs : ((σ : ℝ) + (T : ℝ) * Complex.I) = ρ.1 := sub_eq_zero.mp h0\n have hz := hzne σ\n rw [hs] at hz\n exact hz ρ.2.1\n have hΣcont : Continuous fun σ : ℝ =>\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1) := by\n apply continuous_finset_sum\n intro ρ hρ\n exact Continuous.div continuous_const (hpath.sub continuous_const) (hden ρ hρ)\n have hΣnorm_cont : Continuous fun σ : ℝ =>\n ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=\n continuous_norm.comp hΣcont\n have hΣnorm_int : IntervalIntegrable\n (fun σ : ℝ => ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖)\n MeasureTheory.volume (-5 / 2) 3 := hΣnorm_cont.intervalIntegrable _ _\n have hRcont : Continuous fun σ : ℝ =>\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=\n continuous_norm.comp (hLDc.sub hΣcont)\n have hRnorm_int : IntervalIntegrable\n (fun σ : ℝ => ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖)\n MeasureTheory.volume (-5 / 2) 3 := hRcont.intervalIntegrable _ _\n -- the per-ρ data (δ_ρ := |γ−T| ∈ [c_clear, 1))\n have hρdata : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →\n (0 : ℝ) < |ρ.1.im - T| ∧ |ρ.1.im - T| < 1 ∧\n (1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2))) ≤ |ρ.1.im - T| := by\n intro ρ hρ\n have hδ1 := mem_nearZerosSub.mp hρ\n obtain ⟨hlo, hhi⟩ := abs_lt.mp hδ1\n have hγ1 : Real.sqrt (n : ℝ) - 1 < ρ.1.im := by nlinarith [hTn]\n have hγ2 : ρ.1.im < Real.sqrt (n : ℝ) + 2 := by nlinarith [hTn1]\n have hδge := hTwide ρ.1 ρ.2 hγ1 hγ2\n have hδpos : (0 : ℝ) < |ρ.1.im - T| :=\n lt_of_lt_of_le (one_div_pos.mpr (by positivity :\n (0 : ℝ) < 9 * C0hat (Real.sqrt (n : ℝ) + 2))) hδge\n exact ⟨hδpos, hδ1, hδge⟩\n -- the kernel bound per σ (the ii′-4 shift lemma at s := w − 1)\n have hnT2 : (n : ℝ) ≤ T ^ 2 := by\n have h1 : (Real.sqrt (n : ℝ)) ^ 2 ≤ T ^ 2 :=\n pow_le_pow_left₀ (Real.sqrt_nonneg _) hTn 2\n rwa [Real.sq_sqrt (by positivity : (0 : ℝ) ≤ (n : ℝ))] at h1\n have hker : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →\n ‖kFun n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤ Real.exp 4 + 1 := by\n intro σ hσ\n obtain ⟨hσ1, hσ2⟩ := hσ\n have hre : (((σ : ℝ) + (T : ℝ) * Complex.I) - 1).re = σ - 1 := by simp\n have him : (((σ : ℝ) + (T : ℝ) * Complex.I) - 1).im = T := by simp\n have h1 := kFun_shift_norm_le_exp_four_add_one (n := n)\n (s := (((σ : ℝ) + (T : ℝ) * Complex.I) - 1))\n (by rw [hre]; linarith [hσ2]) (by rw [him]; exact hnT2)\n rwa [sub_add_cancel] at h1\n -- pointwise Jlag ≤ (e⁴+1)·‖logDeriv‖\n have hptJ : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →\n ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤\n (Real.exp 4 + 1) * ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := by\n intro σ hσ\n rw [Jlag_norm_eq]\n exact mul_le_mul (hker σ hσ) le_rfl (norm_nonneg _) (by positivity)\n have hJint : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤\n (Real.exp 4 + 1) * ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := by\n have h := intervalIntegral.integral_mono_on hlen hJintbl hKLintbl\n (fun σ hσ => hptJ σ hσ)\n rwa [intervalIntegral.integral_const_mul] at h\n -- the logDeriv split: ‖logDeriv‖ ≤ ‖Σ‖ + ‖logDeriv − Σ‖\n have hsumcont : Continuous fun σ : ℝ =>\n ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ +\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=\n hΣnorm_cont.add hRcont\n have hsum_intbl : IntervalIntegrable\n (fun σ : ℝ => ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ +\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖)\n MeasureTheory.volume (-5 / 2) 3 := hsumcont.intervalIntegrable _ _\n have hsplit : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤\n (∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖) +\n (∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖) := by\n have hpt2 : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ ≤\n ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ +\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=\n fun σ _ => norm_le_insert' _ _\n have h := intervalIntegral.integral_mono_on hlen hLDintbl hsum_intbl\n (fun σ hσ => hpt2 σ hσ)\n rwa [intervalIntegral.integral_add hΣnorm_int hRnorm_int] at h\n -- the R-part integral (the 5f capstone, constant in σ)\n have hR : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤\n 10.5 * Real.log (T + 2) + 48 := by\n intro σ hσ\n obtain ⟨hσ1, hσ2⟩ := hσ\n have hre : ((σ : ℝ) + (T : ℝ) * Complex.I).re = σ := by simp\n have him : ((σ : ℝ) + (T : ℝ) * Complex.I).im = T := by simp\n have h := logDeriv_riemannZeta_sub_nearZeros_le_tight (t := T)\n (s := ((σ : ℝ) + (T : ℝ) * Complex.I)) hZC hZC2 hNLZ h10T\n (by rw [hre]; exact hσ1) (by rw [hre]; exact hσ2) him (hzne σ)\n rwa [abs_of_nonneg hT0] at h\n have hRint : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48) := by\n have h := intervalIntegral.integral_mono_on hlen hRnorm_int intervalIntegrable_const\n (fun σ hσ => hR σ hσ)\n rwa [intervalIntegral.integral_const, smul_eq_mul] at h\n -- the near-sum integral: the per-zero arcsinh-FTC machine + the swap\n have hnormid : ∀ σ : ℝ, ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ},\n ‖((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1‖ =\n Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2) := by\n intro σ ρ\n have h1 : Complex.normSq (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1) =\n (σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n symm\n rw [Real.sqrt_eq_iff_eq_sq (by positivity) (norm_nonneg _),\n ← Complex.normSq_eq_norm_sq]\n exact h1.symm\n have htermcont : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →\n Continuous fun σ : ℝ => (zeroMult ρ.1 : ℝ) *\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by\n intro ρ hρ\n obtain ⟨hδpos, -, -⟩ := hρdata ρ hρ\n have hh : ∀ σ : ℝ, (0 : ℝ) < (σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2 := by\n intro σ\n have h3 : ρ.1.im - T ≠ 0 := abs_pos.mp hδpos\n have h4 : T - ρ.1.im ≠ 0 := by\n intro h5\n apply h3\n linarith [h5]\n exact add_pos_of_nonneg_of_pos (sq_nonneg _) (sq_pos_of_ne_zero h4)\n apply Continuous.mul continuous_const\n apply Continuous.div continuous_const\n · exact Real.continuous_sqrt.comp (by fun_prop :\n Continuous fun σ : ℝ => (σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)\n · intro σ\n exact ne_of_gt (Real.sqrt_pos.mpr (hh σ))\n -- pointwise: ‖Σ‖ ≤ Σ mult·(1/√)\n have hpt : ∀ σ : ℝ, σ ∈ Set.Icc (-5 / 2 : ℝ) 3 →\n ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by\n intro σ _\n calc ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖\n ≤ ∑ ρ ∈ nearZerosSub T, ‖(zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ :=\n norm_sum_le _ _\n _ = ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) /\n ‖((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1‖ := by\n apply Finset.sum_congr rfl\n intro ρ _\n rw [norm_div]\n have h2 : ‖(zeroMult ρ.1 : ℂ)‖ = (zeroMult ρ.1 : ℝ) := by\n rw [show (zeroMult ρ.1 : ℂ) = ((zeroMult ρ.1 : ℝ) : ℂ) by\n push_cast; ring, Complex.norm_real]\n exact abs_of_nonneg (Nat.cast_nonneg _)\n rw [h2]\n _ = ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by\n apply Finset.sum_congr rfl\n intro ρ _\n rw [hnormid σ ρ, mul_one_div]\n -- the swap ∫Σ = Σ∫\n have hswap : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\n (∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2))) =\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\n 1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by\n rw [intervalIntegral.integral_finsetSum\n (fun ρ hρ => (htermcont ρ hρ).intervalIntegrable _ _)]\n apply Finset.sum_congr rfl\n intro ρ _\n exact intervalIntegral.integral_const_mul _ _\n -- per-ρ: the integral ≤ 2·log(148.5·Ĉ₀(√n+2))\n have hper : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub T →\n (∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\n 1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) ≤\n 2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) := by\n intro ρ hρ\n obtain ⟨hδpos, hδ1, hδge⟩ := hρdata ρ hρ\n have hsq : (T - ρ.1.im) ^ 2 = |ρ.1.im - T| ^ 2 := by\n rw [← sq_abs (ρ.1.im - T)]\n ring\n have hmain := per_zero_integral_le_two_log ρ.2.2.1 ρ.2.2.2 hδpos hδ1.le\n rw [hsq] at hmain ⊢\n have hinv : 1 / |ρ.1.im - T| ≤ 9 * C0hat (Real.sqrt (n : ℝ) + 2) := by\n have h := one_div_le_one_div_of_le (one_div_pos.mpr (by positivity :\n (0 : ℝ) < 9 * C0hat (Real.sqrt (n : ℝ) + 2))) hδge\n rwa [one_div_one_div] at h\n have h1 : (16.5 : ℝ) * (1 / |ρ.1.im - T|) ≤\n 16.5 * (9 * C0hat (Real.sqrt (n : ℝ) + 2)) :=\n mul_le_mul_of_nonneg_left hinv (by norm_num)\n have h2 : (16.5 : ℝ) / |ρ.1.im - T| ≤ 148.5 * C0hat (Real.sqrt (n : ℝ) + 2) := by\n rw [mul_one_div, show (16.5 : ℝ) * (9 * C0hat (Real.sqrt (n : ℝ) + 2)) =\n 148.5 * C0hat (Real.sqrt (n : ℝ) + 2) by ring] at h1\n exact h1\n have h3 : Real.log (16.5 / |ρ.1.im - T|) ≤\n Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) :=\n Real.log_le_log (by positivity) h2\n linarith [hmain, h3]\n -- the sum bound: Σ mult·∫ ≤ (2·log(148.5·Ĉ₀))·Z₂(T)\n have hsum : ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\n 1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) ≤\n (2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) * Z2hat T := by\n calc ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\n 1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2))\n ≤ ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) := by\n apply Finset.sum_le_sum\n intro ρ hρ\n exact mul_le_mul_of_nonneg_left (hper ρ hρ) (Nat.cast_nonneg _)\n _ = (2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) *\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) := by\n rw [← Finset.mul_sum]\n apply Finset.sum_congr rfl\n intro ρ _\n ring\n _ ≤ (2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) * Z2hat T :=\n mul_le_mul_of_nonneg_left (nearZerosSub_mult_sum_le hZC2 h10T) hB0nn\n -- the near-sum integral bound\n have hRHScont : Continuous fun σ : ℝ =>\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2)) := by\n apply continuous_finset_sum\n intro ρ hρ\n exact htermcont ρ hρ\n have hΣbound : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤\n (2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) * Z2hat T := by\n have h1 : ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖ ≤\n ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\n (∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℝ) *\n (1 / Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2))) :=\n intervalIntegral.integral_mono_on hlen hΣnorm_int\n (hRHScont.intervalIntegrable _ _) (fun σ hσ => hpt σ hσ)\n exact h1.trans (hswap.trans_le hsum)\n -- assembly\n unfold HIntegral\n calc ‖∫ x in (-5 / 2 : ℝ)..(3 : ℝ), Jlag n ((x : ℝ) + (T : ℝ) * Complex.I)‖\n ≤ ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I)‖ :=\n intervalIntegral.norm_integral_le_integral_norm hlen\n _ ≤ (Real.exp 4 + 1) * ∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I)‖ := hJint\n _ ≤ (Real.exp 4 + 1) *\n ((∫ σ in (-5 / 2 : ℝ)..(3 : ℝ), ‖∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖) +\n (∫ σ in (-5 / 2 : ℝ)..(3 : ℝ),\n ‖logDeriv riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) -\n ∑ ρ ∈ nearZerosSub T, (zeroMult ρ.1 : ℂ) /\n (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1)‖)) :=\n mul_le_mul_of_nonneg_left hsplit (by positivity)\n _ ≤ (Real.exp 4 + 1) *\n ((2 * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2))) * Z2hat T +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) :=\n mul_le_mul_of_nonneg_left (add_le_add hΣbound hRint) (by positivity)\n _ = (Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by ring\n\n/-- **6-c-iv (the bottom side −T)**: the conj trick (DL-5 pattern). -/\ntheorem hIntegral_Jlag_mid_neg_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n (hNLZ : NoLowZeros) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}\n (hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt (n : ℝ) - 1 < ρ.im →\n ρ.im < Real.sqrt (n : ℝ) + 2 →\n 1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤ |ρ.im - T|)\n (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n ‖HIntegral (Jlag n) (-5 / 2) 3 (-T)‖ ≤\n (Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by\n have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n have hT0 : (0 : ℝ) < T := by\n have h1 : (0 : ℝ) < Real.sqrt (n : ℝ) := Real.sqrt_pos.mpr (by linarith)\n linarith\n have hconj : HIntegral (Jlag n) (-5 / 2) 3 (-T) =\n (starRingEnd ℂ) (HIntegral (Jlag n) (-5 / 2) 3 T) := by\n unfold HIntegral\n rw [← intervalIntegral.intervalIntegral_conj]\n apply intervalIntegral.integral_congr\n intro σ hσ\n show Jlag n ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =\n (starRingEnd ℂ) (Jlag n ((σ : ℝ) + T * Complex.I))\n have hid2 : ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =\n (starRingEnd ℂ) ((σ : ℝ) + T * Complex.I) := by simp\n rw [hid2]\n exact Jlag_conj n (by\n intro h\n have him : (((σ : ℝ) + T * Complex.I)).im = T := by simp\n rw [h] at him\n simp at him\n linarith [hT0])\n rw [hconj, Complex.norm_conj]\n exact hIntegral_Jlag_mid_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1\n\nend NguyenRH1"},"extra_content":null}]