← Session 31 — ii′-5f: tight R-bound 10.5/48 (piece 3 + pinch)
thinking (516 chars)
Now I have the exact ending. Let me write §18 via a python insertion (avoiding the Edit-tool stale-read problem and letting me fix the placeholder). I'll write the section to a temp file and insert before `end NguyenRH1\n\nend`.
Key fixes from the draft:
1. Add `farGRightMaj_nonneg {t} (k) : 0 ≤ farGRightMaj t k` standalone.
2. Add `farGRightMaj_summable {t} (ht : 10 ≤ t) : Summable (farGRightMaj t)` standalone (the hsumm body from series_le), and make series_le use it.
3. farGRight_le's ofReal_tsum uses both.
Writing §18 via python insertion with the summability lemmas properly factored.
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\insert_s18.py",
"content": "p = 'NguyenRH1/LiTightR.lean'\nsrc = open(p, encoding='utf-8').read()\n\nsection18 = '''\n/-! ## 18. Piece 3j: the right-tail machine (\u03b3 > 2t) -/\n\n/-- The right-tail summand: farG restricted to tail zeros (x \u2265 \u230at\u230b\u208a+1)\non the right side (\u03b3 \u2265 t, hence \u03b3 > 2t). -/\ndef farGRight (t : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u211d :=\n if (Nat.floor t + 1 \u2264 |\u03c1.1.im - t| \u2227 t \u2264 \u03c1.1.im) then farG t \u03c1 else 0\n\nlemma farGRight_nonneg (t : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : (0 : \u211d) \u2264 farGRight t \u03c1 := by\n by_cases h : (Nat.floor t + 1 \u2264 |\u03c1.1.im - t| \u2227 t \u2264 \u03c1.1.im)\n \u00b7 rw [farGRight, if_pos h]\n exact farG_nonneg t \u03c1\n \u00b7 rw [farGRight, if_neg h]\n\nlemma farGRight_summable {t : \u211d} (ht : 0 \u2264 t) : Summable (farGRight t) := by\n apply Summable.of_norm_bounded (farG_summable ht)\n intro \u03c1\n rw [Real.norm_eq_abs, abs_of_nonneg (farGRight_nonneg t \u03c1)]\n by_cases h : (Nat.floor t + 1 \u2264 |\u03c1.1.im - t| \u2227 t \u2264 \u03c1.1.im)\n \u00b7 rw [farGRight, if_pos h]\n \u00b7 rw [farGRight, if_neg h]\n exact farG_nonneg t \u03c1\n\n/-- The per-element right-tail bound: farGRight \u2264 4.5\u00b7farW(\u230ax\u230b\u208a)\u00b7m. -/\nlemma farGRight_term_le {t : \u211d} (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n farGRight t \u03c1 \u2264 4.5 * farW (Nat.floor |\u03c1.1.im - t|) * (zeroMult \u03c1.1 : \u211d) := by\n classical\n by_cases h : (Nat.floor t + 1 \u2264 |\u03c1.1.im - t| \u2227 t \u2264 \u03c1.1.im)\n \u00b7 rw [farGRight, if_pos h]\n have hx1 : (1 : \u211d) \u2264 |\u03c1.1.im - t| := by\n have h1 : (1 : \u211d) \u2264 (Nat.floor t : \u211d) + 1 := by\n have h2 : (0 : \u211d) \u2264 (Nat.floor t : \u211d) := Nat.floor_nonneg\n linarith\n have h3 : (Nat.floor t : \u211d) + 1 \u2264 |\u03c1.1.im - t| := by\n have h4 : ((Nat.floor t + 1 : \u2115) : \u211d) \u2264 |\u03c1.1.im - t| := by exact_mod_cast h.1\n have h5 : ((Nat.floor t + 1 : \u2115) : \u211d) = (Nat.floor t : \u211d) + 1 := by push_cast; ring\n rwa [h5] at h4\n linarith [h1, h3]\n exact farG_le_farW_mul \u03c1 hx1\n \u00b7 rw [farGRight, if_neg h]\n positivity\n\n/-- The right-tail fiber {\u230ax\u230b\u208a = k} is finite. -/\nlemma farGRight_fiber_finite {t : \u211d} (ht : 0 \u2264 t) (k : \u2115) :\n ((fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k} :\n Set {\u03c1 : \u2102 // IsNontrivialZero \u03c1}).Finite := by\n apply (finite_subtype_norm_lt (t + (k : \u211d) + 2)).subset\n intro \u03c1 h\u03c1\n show \u2016\u03c1.1\u2016 < t + (k : \u211d) + 2\n have hmem : Nat.floor |\u03c1.1.im - t| = k := h\u03c1\n have h1 : |\u03c1.1.im - t| < (k : \u211d) + 1 := by\n have h2 := Nat.lt_floor_add_one |\u03c1.1.im - t|\n rwa [hmem] at h2\n have hle : \u2016\u03c1.1\u2016 \u2264 |\u03c1.1.re| + |\u03c1.1.im| := Complex.norm_le_abs_re_add_abs_im _\n have hre : |\u03c1.1.re| \u2264 1 := by\n have h3 : 0 < \u03c1.1.re := \u03c1.2.2.1\n have h4 : \u03c1.1.re < 1 := \u03c1.2.2.2\n rw [abs_le]\n constructor <;> linarith\n have him : |\u03c1.1.im| \u2264 t + |\u03c1.1.im - t| := by\n calc |\u03c1.1.im| = |\u03c1.1.im - t + t| := by rw [sub_add_cancel]\n _ \u2264 |\u03c1.1.im - t| + |t| := abs_add_le _ _\n _ = |\u03c1.1.im - t| + t := by rw [abs_of_nonneg ht]\n _ = t + |\u03c1.1.im - t| := by ring\n linarith [hle, hre, him, h1]\n\n/-- **The per-fiber right-tail count**: the mult-weighted count of\nright-tail zeros with bucket k (\u230at\u230b\u208a+1 \u2264 k) is \u2264 C0hat(2k+1). -/\nlemma farGRight_fiber_count (hZC : ZeroCountProp) {t : \u211d} (ht : 10 \u2264 t)\n {k : \u2115} (hk : Nat.floor t + 1 \u2264 k) :\n \u2211 \u03c1 \u2208 (farGRight_fiber_finite (by linarith : (0 : \u211d) \u2264 t) k).toFinset.filter\n (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im), (zeroMult \u03c1.1 : \u211d)\n \u2264 C0hat (2 * (k : \u211d) + 1) := by\n classical\n set FS := (farGRight_fiber_finite (by linarith : (0 : \u211d) \u2264 t) k).toFinset.filter\n (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im) with hFS\n have htk : (2 : \u211d) \u2264 t + (k : \u211d) := by\n have h1 : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith [ht, h1]\n have hcount : ((zeroWindow_finite (t + (k : \u211d))).toFinset.sum fun \u03c1 => zeroMult \u03c1 : \u211d)\n \u2264 C0hat (t + (k : \u211d) + 1) := hZC (t + (k : \u211d)) htk\n have hmono : C0hat (t + (k : \u211d) + 1) \u2264 C0hat (2 * (k : \u211d) + 1) := by\n apply C0hat_mono (by positivity : (1 : \u211d) \u2264 t + (k : \u211d) + 1)\n have h1 : (Nat.floor t : \u211d) + 1 \u2264 (k : \u211d) := by\n have h2 : ((Nat.floor t + 1 : \u2115) : \u211d) \u2264 (k : \u211d) := by exact_mod_cast hk\n have h3 : ((Nat.floor t + 1 : \u2115) : \u211d) = (Nat.floor t : \u211d) + 1 := by push_cast; ring\n rwa [h3] at h2\n have h4 : t \u2264 (k : \u211d) := by\n have h5 : t \u2264 (Nat.floor t : \u211d) + 1 := by\n have h6 := Nat.lt_floor_add_one t\n linarith [h6]\n linarith [h1, h5]\n linarith [h4]\n have hsub : FS.image (fun \u03c1 => \u03c1.1) \u2286 (zeroWindow_finite (t + (k : \u211d))).toFinset := by\n intro z hz\n obtain \u27e8\u03c1, h\u03c1, rfl\u27e9 := Finset.mem_image.mp hz\n rw [hFS, Finset.mem_filter] at h\u03c1\n obtain \u27e8hmem, him\u27e9 := h\u03c1\n rw [Set.Finite.mem_toFinset] at hmem\n have hmem2 : Nat.floor |\u03c1.1.im - t| = k := hmem\n have hxk : (k : \u211d) \u2264 |\u03c1.1.im - t| := by\n have h1 := Nat.floor_le (abs_nonneg (\u03c1.1.im - t))\n rwa [hmem2] at h1\n have hxk1 : |\u03c1.1.im - t| < (k : \u211d) + 1 := by\n have h1 := Nat.lt_floor_add_one |\u03c1.1.im - t|\n rwa [hmem2] at h1\n have hx : |\u03c1.1.im - t| = \u03c1.1.im - t := abs_of_nonneg (by linarith [him])\n rw [Set.Finite.mem_toFinset]\n refine \u27e8\u03c1.2, ?_, ?_\u27e9\n \u00b7 rw [hx] at hxk\n linarith [hxk, him]\n \u00b7 rw [hx] at hxk1\n linarith [hxk1, him]\n have hbridge : \u2211 \u03c1 \u2208 FS, (zeroMult \u03c1.1 : \u211d)\n = \u2211 \u03c1 \u2208 FS.image (fun \u03c1 => \u03c1.1), (zeroMult \u03c1 : \u211d) := by\n rw [Finset.sum_image (fun x _ y _ h => Subtype.ext h)]\n calc \u2211 \u03c1 \u2208 FS, (zeroMult \u03c1.1 : \u211d)\n = \u2211 z \u2208 FS.image (fun \u03c1 => \u03c1.1), (zeroMult z : \u211d) := hbridge\n _ \u2264 \u2211 z \u2208 (zeroWindow_finite (t + (k : \u211d))).toFinset, (zeroMult z : \u211d) :=\n Finset.sum_le_sum_of_subset_of_nonneg hsub (fun z _ _ => Nat.cast_nonneg _)\n _ = (((zeroWindow_finite (t + (k : \u211d))).toFinset.sum fun \u03c1 => zeroMult \u03c1) : \u211d) := rfl\n _ \u2264 C0hat (t + (k : \u211d) + 1) := hcount\n _ \u2264 C0hat (2 * (k : \u211d) + 1) := hmono\n\n/-- The per-fiber right-tail bound (ENNReal form). -/\nlemma farGRight_fiber_le (hZC : ZeroCountProp) {t : \u211d} (ht : 10 \u2264 t) (k : \u2115) :\n \u2211' b : (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k},\n ENNReal.ofReal (farGRight t b.1)\n \u2264 ENNReal.ofReal (if Nat.floor t + 1 \u2264 k then 4.5 * farW k * C0hat (2 * (k : \u211d) + 1) else 0) := by\n classical\n have hfin : ((fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k} :\n Set {\u03c1 : \u2102 // IsNontrivialZero \u03c1}).Finite := farGRight_fiber_finite (by linarith : (0 : \u211d) \u2264 t) k\n have htsum : \u2211' b : (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k},\n ENNReal.ofReal (farGRight t b.1)\n = \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n ((fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k}).indicator\n (fun \u03c1 => ENNReal.ofReal (farGRight t \u03c1)) \u03c1 :=\n tsum_subtype _ (fun \u03c1 => ENNReal.ofReal (farGRight t \u03c1))\n rw [htsum]\n rw [tsum_eq_sum (s := hfin.toFinset) (fun \u03c1 h\u03c1 => by\n apply Set.indicator_of_notMem\n rwa [Set.Finite.mem_toFinset] at h\u03c1)]\n rw [Finset.sum_congr rfl (fun \u03c1 h\u03c1 =>\n Set.indicator_of_mem (by rwa [Set.Finite.mem_toFinset] at h\u03c1) _)]\n rw [\u2190 ENNReal.ofReal_sum_of_nonneg (fun \u03c1 _ => farGRight_nonneg t \u03c1)]\n apply ENNReal.ofReal_le_ofReal\n by_cases hk : Nat.floor t + 1 \u2264 k\n \u00b7 rw [if_pos hk]\n rw [\u2190 Finset.sum_filter_add_sum_filter_not hfin.toFinset\n (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im) (farGRight t)]\n have hzero : \u2211 \u03c1 \u2208 hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n \u00ac t \u2264 \u03c1.1.im), farGRight t \u03c1 = 0 := by\n apply Finset.sum_eq_zero\n intro \u03c1 h\u03c1\n rw [Finset.mem_filter] at h\u03c1\n rw [farGRight, if_neg (fun h => h\u03c1.2 h.2)]\n rw [hzero, add_zero]\n calc \u2211 \u03c1 \u2208 hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im),\n farGRight t \u03c1\n \u2264 \u2211 \u03c1 \u2208 hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im),\n (4.5 * farW k) * (zeroMult \u03c1.1 : \u211d) := by\n apply Finset.sum_le_sum\n intro \u03c1 h\u03c1\n have h1 := farGRight_term_le \u03c1\n rw [Finset.mem_filter] at h\u03c1\n obtain \u27e8hmem, _\u27e9 := h\u03c1\n rw [Set.Finite.mem_toFinset] at hmem\n have hmem2 : Nat.floor |\u03c1.1.im - t| = k := hmem\n rw [hmem2] at h1\n exact h1\n _ = (4.5 * farW k) *\n \u2211 \u03c1 \u2208 hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im),\n (zeroMult \u03c1.1 : \u211d) := by\n rw [Finset.mul_sum]\n _ \u2264 (4.5 * farW k) * C0hat (2 * (k : \u211d) + 1) :=\n mul_le_mul_of_nonneg_left (farGRight_fiber_count hZC ht hk)\n (mul_nonneg (by norm_num : (0 : \u211d) \u2264 4.5) (farW_nonneg k))\n \u00b7 rw [if_neg hk]\n apply le_of_eq\n apply Finset.sum_eq_zero\n intro \u03c1 h\u03c1\n rw [Set.Finite.mem_toFinset] at h\u03c1\n have hmem2 : Nat.floor |\u03c1.1.im - t| = k := h\u03c1\n rw [farGRight, if_neg (fun h => hk (by\n have h1 : ((Nat.floor t + 1 : \u2115) : \u211d) \u2264 (k : \u211d) := by exact_mod_cast h.1\n have h2 : (Nat.floor t : \u211d) + 1 \u2264 (k : \u211d) := by\n have h3 : ((Nat.floor t + 1 : \u2115) : \u211d) = (Nat.floor t : \u211d) + 1 := by push_cast; ring\n rwa [h3] at h1\n have h4 : (Nat.floor t : \u211d) + 1 \u2264 |\u03c1.1.im - t| := by\n have h5 : (k : \u211d) \u2264 |\u03c1.1.im - t| := by\n have h6 := Nat.floor_le (abs_nonneg (\u03c1.1.im - t))\n rwa [hmem2] at h6\n linarith [h2, h5]\n exact h4 : Nat.floor t + 1 \u2264 |\u03c1.1.im - t|))]\n\n/-- loglog k \u2265 \u22120.37 for k \u2265 1 (the bridge nonnegativity input). -/\nlemma loglog_ge_neg_point37 {k : \u2115} (hk : 1 \u2264 k) :\n (-0.37 : \u211d) \u2264 Real.log (Real.log k) := by\n rcases eq_or_ne k 1 with rfl | hk1\n \u00b7 simp [Real.log_one, Real.log_zero]\n \u00b7 have hk2 : 2 \u2264 k := by omega\n have h1 : (0.693 : \u211d) \u2264 Real.log 2 := Real.log_two_gt_d9.le.trans (by norm_num)\n have h2 : (0.693 : \u211d) \u2264 Real.log k := by\n have h3 : Real.log 2 \u2264 Real.log k :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 2) (by exact_mod_cast hk2)\n linarith [h1, h3]\n have h4 : Real.log 0.693 \u2264 Real.log (Real.log k) :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 0.693) h2\n have h5 : (-0.37 : \u211d) \u2264 Real.log 0.693 := by\n have h6 : (1 / 0.693 : \u211d) \u2264 Real.exp 0.37 := by\n have h7 := Real.sum_le_exp_of_nonneg (show (0 : \u211d) \u2264 0.37 by norm_num) 5\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h7\n norm_num at h7\n have h8 : (1 / 0.693 : \u211d) \u2264 1.447671 := by norm_num\n linarith [h7, h8]\n have h7 : Real.log (1 / 0.693) \u2264 0.37 := by\n have h8 := Real.log_le_log (by norm_num : (0 : \u211d) < 1 / 0.693) h6\n rwa [Real.log_exp] at h8\n rw [Real.log_div (by norm_num : (1 : \u211d) \u2260 0) (by norm_num : (0.693 : \u211d) \u2260 0),\n Real.log_one] at h7\n linarith [h7]\n linarith [h4, h5]\n\n/-- The right-tail bridge is nonnegative for all k. -/\nlemma farGRightBridge_nonneg (k : \u2115) :\n (0 : \u211d) \u2264 0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9 := by\n by_cases hk0 : k = 0\n \u00b7 rw [hk0]\n simp only [Nat.cast_zero, Real.log_zero, Real.log_one, add_zero]\n norm_num\n \u00b7 have hk1 : 1 \u2264 k := by omega\n have h1 : (0 : \u211d) \u2264 Real.log k := Real.log_nonneg (by exact_mod_cast hk1 : (1 : \u211d) \u2264 (k : \u211d))\n have h2 := loglog_ge_neg_point37 hk1\n have h3 : (0 : \u211d) \u2264 (0.433 : \u211d) * (Real.log k + 0.833) := by\n apply mul_nonneg (by norm_num)\n linarith [h1]\n have h4 : (0.886 : \u211d) * ((-0.37 : \u211d) + 0.3475) \u2264 0.886 * (Real.log (Real.log k) + 0.3475) :=\n mul_le_mul_of_nonneg_left (by linarith [h2] : (-0.37 : \u211d) + 0.3475\n \u2264 Real.log (Real.log k) + 0.3475) (by norm_num)\n have h5 : (0.433 : \u211d) * 0.833 \u2264 0.433 * (Real.log k + 0.833) :=\n mul_le_mul_of_nonneg_left (by linarith [h1] : (0.833 : \u211d) \u2264 Real.log k + 0.833) (by norm_num)\n linarith [h3, h4, h5]\n\n/-- The right-tail majorant series (if-form on \u2115). -/\ndef farGRightMaj (t : \u211d) : \u2115 \u2192 \u211d := fun k =>\n if Nat.floor t + 1 \u2264 k then 4.5 * farW k * C0hat (2 * (k : \u211d) + 1) else 0\n\nlemma farGRightMaj_nonneg {t : \u211d} (k : \u2115) : (0 : \u211d) \u2264 farGRightMaj t k := by\n by_cases hk : Nat.floor t + 1 \u2264 k\n \u00b7 rw [farGRightMaj, if_pos hk]\n have h1 : (1 : \u211d) \u2264 (k : \u211d) + 1 + 1 := by\n have h2 : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith\n have h3 := two_le_C0hat h1\n have h4 : (0 : \u211d) \u2264 4.5 * farW k := by positivity\n exact mul_nonneg h4 (by linarith [h3])\n \u00b7 rw [farGRightMaj, if_neg hk]\n\n/-- The right-tail combo form (the brick decomposition target). -/\ndef farGRightMajCombo : \u2115 \u2192 \u211d := fun k =>\n 4.5 * (1 / (k : \u211d) ^ 2) * (0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9)\n\nlemma farGRightMajCombo_nonneg (k : \u2115) : (0 : \u211d) \u2264 farGRightMajCombo k := by\n rw [farGRightMajCombo]\n have h := farGRightBridge_nonneg k\n have h2 : (0 : \u211d) \u2264 4.5 * (1 / (k : \u211d) ^ 2) := by positivity\n exact mul_nonneg h2 h\n\n/-- The pointwise combo bound for the farGRightMaj. -/\nlemma farGRightMaj_le_combo {t : \u211d} (ht : 10 \u2264 t) (k : \u2115) :\n farGRightMaj t k \u2264 farGRightMajCombo k := by\n by_cases hk : Nat.floor t + 1 \u2264 k\n \u00b7 rw [farGRightMaj, if_pos hk, farGRightMajCombo]\n have hk11 : 11 \u2264 k := by\n have h1 : 10 \u2264 Nat.floor t := by\n have h2 := Nat.floor_mono (by norm_num : (10 : \u211d) \u2264 t)\n rwa [Nat.floor_ofNat] at h2\n omega\n have h1 := C0hat_two_mul_add_one_le hk11\n have h2 := farW_le_inv_sq (by omega : 1 \u2264 k)\n have hnn := farGRightBridge_nonneg k\n have h4 : 4.5 * farW k \u2264 4.5 * (1 / (k : \u211d) ^ 2) :=\n mul_le_mul_of_nonneg_left h2 (by norm_num : (0 : \u211d) \u2264 4.5)\n calc 4.5 * farW k * C0hat (2 * (k : \u211d) + 1)\n \u2264 (4.5 * (1 / (k : \u211d) ^ 2)) * (0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9) := by\n apply mul_le_mul h4 h1 hnn (by positivity : (0 : \u211d) \u2264 4.5 * (1 / (k : \u211d) ^ 2))\n \u00b7 rw [farGRightMaj, if_neg hk]\n exact farGRightMajCombo_nonneg k\n\n/-- The shifted LA\u2080-family for k \u2265 11 is summable. -/\nlemma tail11_inv_sq_summable :\n Summable (fun k : \u2115 => (1 : \u211d) / ((k : \u211d) + 11) ^ 2) := by\n have h := antitoneOn_one_div_sq.summable_of_integrableOn_Ioi\n integrableOn_one_div_sq (fun t ht => by\n have ht10 : (10 : \u211d) < t := ht\n positivity)\n have h2 := (summable_nat_add_iff (f := fun n : \u2115 => (1 : \u211d) / (n : \u211d) ^ 2) 11).mpr h\n refine h2.congr fun n => ?_\n push_cast\n ring_nf\n\n/-- The shifted LA\u2082-family for k \u2265 11 is summable. -/\nlemma tail11_loglog_div_sq_summable :\n Summable (fun k : \u2115 =>\n Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2) := by\n apply Summable.of_norm_bounded (tail11_log_div_sq_summable.mul_left (1 / Real.exp 1))\n intro k\n rw [Real.norm_eq_abs]\n rw [abs_of_nonneg (by\n have hk1 : (1 : \u211d) \u2264 Real.log ((k : \u211d) + 11) := by\n have h1 := log_eleven_ge\n have h2 : Real.log 11 \u2264 Real.log ((k : \u211d) + 11) :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 11) (by\n have h : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith)\n linarith [h1, h2]\n have h3 : (0 : \u211d) \u2264 Real.log (Real.log ((k : \u211d) + 11)) := Real.log_nonneg hk1\n positivity : (0 : \u211d) \u2264 Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2)]\n have hk1 : (1 : \u211d) < (k : \u211d) + 11 := by\n have h : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith\n have h4 := log_log_le_div_exp hk1\n have h5 : (0 : \u211d) \u2264 ((k : \u211d) + 11) ^ 2 := by positivity\n have h6 := div_le_div_of_nonneg_right h4 h5\n rw [mul_div_assoc] at h6\n exact h6\n\n/-- The shifted combo is summable (RW-brick families). -/\nlemma farGRightMajCombo_shift_summable :\n Summable (fun k : \u2115 => farGRightMajCombo (k + 11)) := by\n have hAB : Summable (fun k : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((k : \u211d) + 11) / ((k : \u211d) + 11) ^ 2)) :=\n (tail11_inv_sq_summable.mul_left _).add (tail11_log_div_sq_summable.mul_left _)\n have hABC : Summable (fun k : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((k : \u211d) + 11) / ((k : \u211d) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2)) :=\n hAB.add (tail11_loglog_div_sq_summable.mul_left _)\n have hsum := hABC.mul_left 4.5\n apply Summable.congr hsum\n intro k\n rw [farGRightMajCombo]\n have hcast : ((k + 11 : \u2115) : \u211d) = (k : \u211d) + 11 := by push_cast; ring\n rw [hcast]\n ring\n\nlemma farGRightMaj_summable {t : \u211d} (ht : 10 \u2264 t) : Summable (farGRightMaj t) := by\n apply (summable_nat_add_iff (f := farGRightMaj t) 11).mp\n apply Summable.of_norm_bounded farGRightMajCombo_shift_summable\n intro k\n rw [Real.norm_eq_abs, abs_of_nonneg (farGRightMaj_nonneg (k + 11))]\n exact farGRightMaj_le_combo ht (k + 11)\n\n/-- **The right-tail series bound**. -/\nlemma farGRightMaj_series_le {t : \u211d} (ht : 10 \u2264 t) :\n (\u2211' k : \u2115, farGRightMaj t k)\n \u2264 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n have hsplit : (\u2211' k : \u2115, farGRightMaj t k)\n = (\u2211 k \u2208 Finset.range 11, farGRightMaj t k) + \u2211' k : \u2115, farGRightMaj t (k + 11) :=\n ((farGRightMaj_summable ht).sum_add_tsum_nat_add 11).symm\n have hzero : \u2211 k \u2208 Finset.range 11, farGRightMaj t k = 0 := by\n apply Finset.sum_eq_zero\n intro k hk\n rw [Finset.mem_range] at hk\n rw [farGRightMaj, if_neg (by\n have h1 : 10 \u2264 Nat.floor t := by\n have h2 := Nat.floor_mono (by norm_num : (10 : \u211d) \u2264 t)\n rwa [Nat.floor_ofNat] at h2\n omega : \u00acNat.floor t + 1 \u2264 k)]\n have hle := Summable.tsum_le_tsum (fun k => farGRightMaj_le_combo ht (k + 11))\n (farGRightMaj_summable ht) farGRightMajCombo_shift_summable\n have hW0 := tail11_inv_sq_le\n have hW1 := tail11_log_div_sq_le\n have hW2 := tail11_loglog_div_sq_le\n have heval : (\u2211' k : \u2115,\n 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((k : \u211d) + 11) / ((k : \u211d) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2)))\n \u2264 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * 0.1\n + 0.433 * 0.3303 + 0.886 * 0.1216) := by\n rw [tsum_mul_left]\n apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : \u211d) \u2264 4.5)\n have hdecomp : (\u2211' x : \u2115,\n ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2)))\n = (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (\u2211' x : \u2115, (1 / ((x : \u211d) + 11) ^ 2))\n + 0.433 * (\u2211' x : \u2115, (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2))\n + 0.886 * (\u2211' x : \u2115, (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2)) := by\n have e1 := Summable.tsum_add\n (f := fun x : \u2115 => (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2))\n (g := fun x : \u2115 => 0.886 * (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2))\n ((tail11_inv_sq_summable.mul_left _).add (tail11_log_div_sq_summable.mul_left _))\n (tail11_loglog_div_sq_summable.mul_left _)\n have e2 := Summable.tsum_add\n (f := fun x : \u2115 => (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2))\n (g := fun x : \u2115 => 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2))\n (tail11_inv_sq_summable.mul_left _) (tail11_log_div_sq_summable.mul_left _)\n rw [show (\u2211' x : \u2115,\n ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2)))\n = \u2211' x : \u2115, ((fun x : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)) x\n + (fun x : \u2115 => 0.886 * (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2)) x)\n from rfl]\n rw [e1]\n rw [show (\u2211' x : \u2115, (fun x : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)) x)\n = \u2211' x : \u2115, ((fun x : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)) x\n + (fun x : \u2115 => 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)) x)\n from rfl]\n rw [e2, tsum_mul_left, tsum_mul_left, tsum_mul_left]\n rw [hdecomp]\n have hle1 := mul_le_mul_of_nonneg_left hW0 (by positivity : (0 : \u211d) \u2264\n 0.433 * 0.833 + 0.886 * 0.3475 + 2.9)\n have hle2 := mul_le_mul_of_nonneg_left hW1 (by positivity : (0 : \u211d) \u2264 0.433)\n have hle3 := mul_le_mul_of_nonneg_left hW2 (by positivity : (0 : \u211d) \u2264 0.886)\n linarith [hle1, hle2, hle3]\n calc (\u2211' k : \u2115, farGRightMaj t k)\n = (\u2211 k \u2208 Finset.range 11, farGRightMaj t k) + \u2211' k : \u2115, farGRightMaj t (k + 11) := hsplit\n _ = 0 + \u2211' k : \u2115, farGRightMaj t (k + 11) := by rw [hzero]\n _ \u2264 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * 0.1\n + 0.433 * 0.3303 + 0.886 * 0.1216) := by linarith [hle, heval]\n _ = 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by ring\n\n/-- **The right-tail bound** (the ENNReal fiberwise assembly). -/\nlemma farGRight_le (hZC : ZeroCountProp) {t : \u211d} (ht : 10 \u2264 t) :\n \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, farGRight t \u03c1\n \u2264 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n have hC0 : (0 : \u211d) \u2264 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n positivity\n rw [\u2190 ENNReal.ofReal_le_ofReal_iff hC0]\n rw [ENNReal.ofReal_tsum_of_nonneg (fun \u03c1 => farGRight_nonneg t \u03c1)\n (farGRight_summable (by linarith : (0 : \u211d) \u2264 t))]\n rw [\u2190 ENNReal.tsum_fiberwise (fun \u03c1 => ENNReal.ofReal (farGRight t \u03c1))\n (fun \u03c1 => Nat.floor |\u03c1.1.im - t|)]\n have hper : \u2200 k : \u2115, \u2211' b : (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k},\n ENNReal.ofReal (farGRight t b.1)\n \u2264 ENNReal.ofReal (farGRightMaj t k) := by\n intro k\n have h := farGRight_fiber_le hZC ht k\n rwa [farGRightMaj] at *\n calc \u2211' j : \u2115, \u2211' b : (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {j},\n ENNReal.ofReal (farGRight t b.1)\n \u2264 \u2211' j : \u2115, ENNReal.ofReal (farGRightMaj t j) := ENNReal.tsum_le_tsum hper\n _ = ENNReal.ofReal (\u2211' j : \u2115, farGRightMaj t j) := by\n rw [ENNReal.ofReal_tsum_of_nonneg (fun k => farGRightMaj_nonneg k)\n (farGRightMaj_summable ht)]\n _ \u2264 ENNReal.ofReal (4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1)) :=\n ENNReal.ofReal_le_ofReal (farGRightMaj_series_le ht)\n\nend NguyenRH1\n\nend'''\n\nanchor = \"end NguyenRH1\\n\\nend\"\nassert src.count(anchor) == 1\nsrc = src.replace(anchor, section18)\nopen(p, 'w', encoding='utf-8').write(src)\nprint(\"inserted section 18\")\n"
}
result 2026-08-24 20:33:38Z → 2026-08-24 20:33:38Z
{
"type": "create",
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\insert_s18.py",
"content": "p = 'NguyenRH1/LiTightR.lean'\nsrc = open(p, encoding='utf-8').read()\n\nsection18 = '''\n/-! ## 18. Piece 3j: the right-tail machine (\u03b3 > 2t) -/\n\n/-- The right-tail summand: farG restricted to tail zeros (x \u2265 \u230at\u230b\u208a+1)\non the right side (\u03b3 \u2265 t, hence \u03b3 > 2t). -/\ndef farGRight (t : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u211d :=\n if (Nat.floor t + 1 \u2264 |\u03c1.1.im - t| \u2227 t \u2264 \u03c1.1.im) then farG t \u03c1 else 0\n\nlemma farGRight_nonneg (t : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : (0 : \u211d) \u2264 farGRight t \u03c1 := by\n by_cases h : (Nat.floor t + 1 \u2264 |\u03c1.1.im - t| \u2227 t \u2264 \u03c1.1.im)\n \u00b7 rw [farGRight, if_pos h]\n exact farG_nonneg t \u03c1\n \u00b7 rw [farGRight, if_neg h]\n\nlemma farGRight_summable {t : \u211d} (ht : 0 \u2264 t) : Summable (farGRight t) := by\n apply Summable.of_norm_bounded (farG_summable ht)\n intro \u03c1\n rw [Real.norm_eq_abs, abs_of_nonneg (farGRight_nonneg t \u03c1)]\n by_cases h : (Nat.floor t + 1 \u2264 |\u03c1.1.im - t| \u2227 t \u2264 \u03c1.1.im)\n \u00b7 rw [farGRight, if_pos h]\n \u00b7 rw [farGRight, if_neg h]\n exact farG_nonneg t \u03c1\n\n/-- The per-element right-tail bound: farGRight \u2264 4.5\u00b7farW(\u230ax\u230b\u208a)\u00b7m. -/\nlemma farGRight_term_le {t : \u211d} (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n farGRight t \u03c1 \u2264 4.5 * farW (Nat.floor |\u03c1.1.im - t|) * (zeroMult \u03c1.1 : \u211d) := by\n classical\n by_cases h : (Nat.floor t + 1 \u2264 |\u03c1.1.im - t| \u2227 t \u2264 \u03c1.1.im)\n \u00b7 rw [farGRight, if_pos h]\n have hx1 : (1 : \u211d) \u2264 |\u03c1.1.im - t| := by\n have h1 : (1 : \u211d) \u2264 (Nat.floor t : \u211d) + 1 := by\n have h2 : (0 : \u211d) \u2264 (Nat.floor t : \u211d) := Nat.floor_nonneg\n linarith\n have h3 : (Nat.floor t : \u211d) + 1 \u2264 |\u03c1.1.im - t| := by\n have h4 : ((Nat.floor t + 1 : \u2115) : \u211d) \u2264 |\u03c1.1.im - t| := by exact_mod_cast h.1\n have h5 : ((Nat.floor t + 1 : \u2115) : \u211d) = (Nat.floor t : \u211d) + 1 := by push_cast; ring\n rwa [h5] at h4\n linarith [h1, h3]\n exact farG_le_farW_mul \u03c1 hx1\n \u00b7 rw [farGRight, if_neg h]\n positivity\n\n/-- The right-tail fiber {\u230ax\u230b\u208a = k} is finite. -/\nlemma farGRight_fiber_finite {t : \u211d} (ht : 0 \u2264 t) (k : \u2115) :\n ((fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k} :\n Set {\u03c1 : \u2102 // IsNontrivialZero \u03c1}).Finite := by\n apply (finite_subtype_norm_lt (t + (k : \u211d) + 2)).subset\n intro \u03c1 h\u03c1\n show \u2016\u03c1.1\u2016 < t + (k : \u211d) + 2\n have hmem : Nat.floor |\u03c1.1.im - t| = k := h\u03c1\n have h1 : |\u03c1.1.im - t| < (k : \u211d) + 1 := by\n have h2 := Nat.lt_floor_add_one |\u03c1.1.im - t|\n rwa [hmem] at h2\n have hle : \u2016\u03c1.1\u2016 \u2264 |\u03c1.1.re| + |\u03c1.1.im| := Complex.norm_le_abs_re_add_abs_im _\n have hre : |\u03c1.1.re| \u2264 1 := by\n have h3 : 0 < \u03c1.1.re := \u03c1.2.2.1\n have h4 : \u03c1.1.re < 1 := \u03c1.2.2.2\n rw [abs_le]\n constructor <;> linarith\n have him : |\u03c1.1.im| \u2264 t + |\u03c1.1.im - t| := by\n calc |\u03c1.1.im| = |\u03c1.1.im - t + t| := by rw [sub_add_cancel]\n _ \u2264 |\u03c1.1.im - t| + |t| := abs_add_le _ _\n _ = |\u03c1.1.im - t| + t := by rw [abs_of_nonneg ht]\n _ = t + |\u03c1.1.im - t| := by ring\n linarith [hle, hre, him, h1]\n\n/-- **The per-fiber right-tail count**: the mult-weighted count of\nright-tail zeros with bucket k (\u230at\u230b\u208a+1 \u2264 k) is \u2264 C0hat(2k+1). -/\nlemma farGRight_fiber_count (hZC : ZeroCountProp) {t : \u211d} (ht : 10 \u2264 t)\n {k : \u2115} (hk : Nat.floor t + 1 \u2264 k) :\n \u2211 \u03c1 \u2208 (farGRight_fiber_finite (by linarith : (0 : \u211d) \u2264 t) k).toFinset.filter\n (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im), (zeroMult \u03c1.1 : \u211d)\n \u2264 C0hat (2 * (k : \u211d) + 1) := by\n classical\n set FS := (farGRight_fiber_finite (by linarith : (0 : \u211d) \u2264 t) k).toFinset.filter\n (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im) with hFS\n have htk : (2 : \u211d) \u2264 t + (k : \u211d) := by\n have h1 : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith [ht, h1]\n have hcount : ((zeroWindow_finite (t + (k : \u211d))).toFinset.sum fun \u03c1 => zeroMult \u03c1 : \u211d)\n \u2264 C0hat (t + (k : \u211d) + 1) := hZC (t + (k : \u211d)) htk\n have hmono : C0hat (t + (k : \u211d) + 1) \u2264 C0hat (2 * (k : \u211d) + 1) := by\n apply C0hat_mono (by positivity : (1 : \u211d) \u2264 t + (k : \u211d) + 1)\n have h1 : (Nat.floor t : \u211d) + 1 \u2264 (k : \u211d) := by\n have h2 : ((Nat.floor t + 1 : \u2115) : \u211d) \u2264 (k : \u211d) := by exact_mod_cast hk\n have h3 : ((Nat.floor t + 1 : \u2115) : \u211d) = (Nat.floor t : \u211d) + 1 := by push_cast; ring\n rwa [h3] at h2\n have h4 : t \u2264 (k : \u211d) := by\n have h5 : t \u2264 (Nat.floor t : \u211d) + 1 := by\n have h6 := Nat.lt_floor_add_one t\n linarith [h6]\n linarith [h1, h5]\n linarith [h4]\n have hsub : FS.image (fun \u03c1 => \u03c1.1) \u2286 (zeroWindow_finite (t + (k : \u211d))).toFinset := by\n intro z hz\n obtain \u27e8\u03c1, h\u03c1, rfl\u27e9 := Finset.mem_image.mp hz\n rw [hFS, Finset.mem_filter] at h\u03c1\n obtain \u27e8hmem, him\u27e9 := h\u03c1\n rw [Set.Finite.mem_toFinset] at hmem\n have hmem2 : Nat.floor |\u03c1.1.im - t| = k := hmem\n have hxk : (k : \u211d) \u2264 |\u03c1.1.im - t| := by\n have h1 := Nat.floor_le (abs_nonneg (\u03c1.1.im - t))\n rwa [hmem2] at h1\n have hxk1 : |\u03c1.1.im - t| < (k : \u211d) + 1 := by\n have h1 := Nat.lt_floor_add_one |\u03c1.1.im - t|\n rwa [hmem2] at h1\n have hx : |\u03c1.1.im - t| = \u03c1.1.im - t := abs_of_nonneg (by linarith [him])\n rw [Set.Finite.mem_toFinset]\n refine \u27e8\u03c1.2, ?_, ?_\u27e9\n \u00b7 rw [hx] at hxk\n linarith [hxk, him]\n \u00b7 rw [hx] at hxk1\n linarith [hxk1, him]\n have hbridge : \u2211 \u03c1 \u2208 FS, (zeroMult \u03c1.1 : \u211d)\n = \u2211 \u03c1 \u2208 FS.image (fun \u03c1 => \u03c1.1), (zeroMult \u03c1 : \u211d) := by\n rw [Finset.sum_image (fun x _ y _ h => Subtype.ext h)]\n calc \u2211 \u03c1 \u2208 FS, (zeroMult \u03c1.1 : \u211d)\n = \u2211 z \u2208 FS.image (fun \u03c1 => \u03c1.1), (zeroMult z : \u211d) := hbridge\n _ \u2264 \u2211 z \u2208 (zeroWindow_finite (t + (k : \u211d))).toFinset, (zeroMult z : \u211d) :=\n Finset.sum_le_sum_of_subset_of_nonneg hsub (fun z _ _ => Nat.cast_nonneg _)\n _ = (((zeroWindow_finite (t + (k : \u211d))).toFinset.sum fun \u03c1 => zeroMult \u03c1) : \u211d) := rfl\n _ \u2264 C0hat (t + (k : \u211d) + 1) := hcount\n _ \u2264 C0hat (2 * (k : \u211d) + 1) := hmono\n\n/-- The per-fiber right-tail bound (ENNReal form). -/\nlemma farGRight_fiber_le (hZC : ZeroCountProp) {t : \u211d} (ht : 10 \u2264 t) (k : \u2115) :\n \u2211' b : (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k},\n ENNReal.ofReal (farGRight t b.1)\n \u2264 ENNReal.ofReal (if Nat.floor t + 1 \u2264 k then 4.5 * farW k * C0hat (2 * (k : \u211d) + 1) else 0) := by\n classical\n have hfin : ((fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k} :\n Set {\u03c1 : \u2102 // IsNontrivialZero \u03c1}).Finite := farGRight_fiber_finite (by linarith : (0 : \u211d) \u2264 t) k\n have htsum : \u2211' b : (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k},\n ENNReal.ofReal (farGRight t b.1)\n = \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n ((fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k}).indicator\n (fun \u03c1 => ENNReal.ofReal (farGRight t \u03c1)) \u03c1 :=\n tsum_subtype _ (fun \u03c1 => ENNReal.ofReal (farGRight t \u03c1))\n rw [htsum]\n rw [tsum_eq_sum (s := hfin.toFinset) (fun \u03c1 h\u03c1 => by\n apply Set.indicator_of_notMem\n rwa [Set.Finite.mem_toFinset] at h\u03c1)]\n rw [Finset.sum_congr rfl (fun \u03c1 h\u03c1 =>\n Set.indicator_of_mem (by rwa [Set.Finite.mem_toFinset] at h\u03c1) _)]\n rw [\u2190 ENNReal.ofReal_sum_of_nonneg (fun \u03c1 _ => farGRight_nonneg t \u03c1)]\n apply ENNReal.ofReal_le_ofReal\n by_cases hk : Nat.floor t + 1 \u2264 k\n \u00b7 rw [if_pos hk]\n rw [\u2190 Finset.sum_filter_add_sum_filter_not hfin.toFinset\n (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im) (farGRight t)]\n have hzero : \u2211 \u03c1 \u2208 hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n \u00ac t \u2264 \u03c1.1.im), farGRight t \u03c1 = 0 := by\n apply Finset.sum_eq_zero\n intro \u03c1 h\u03c1\n rw [Finset.mem_filter] at h\u03c1\n rw [farGRight, if_neg (fun h => h\u03c1.2 h.2)]\n rw [hzero, add_zero]\n calc \u2211 \u03c1 \u2208 hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im),\n farGRight t \u03c1\n \u2264 \u2211 \u03c1 \u2208 hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im),\n (4.5 * farW k) * (zeroMult \u03c1.1 : \u211d) := by\n apply Finset.sum_le_sum\n intro \u03c1 h\u03c1\n have h1 := farGRight_term_le \u03c1\n rw [Finset.mem_filter] at h\u03c1\n obtain \u27e8hmem, _\u27e9 := h\u03c1\n rw [Set.Finite.mem_toFinset] at hmem\n have hmem2 : Nat.floor |\u03c1.1.im - t| = k := hmem\n rw [hmem2] at h1\n exact h1\n _ = (4.5 * farW k) *\n \u2211 \u03c1 \u2208 hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => t \u2264 \u03c1.1.im),\n (zeroMult \u03c1.1 : \u211d) := by\n rw [Finset.mul_sum]\n _ \u2264 (4.5 * farW k) * C0hat (2 * (k : \u211d) + 1) :=\n mul_le_mul_of_nonneg_left (farGRight_fiber_count hZC ht hk)\n (mul_nonneg (by norm_num : (0 : \u211d) \u2264 4.5) (farW_nonneg k))\n \u00b7 rw [if_neg hk]\n apply le_of_eq\n apply Finset.sum_eq_zero\n intro \u03c1 h\u03c1\n rw [Set.Finite.mem_toFinset] at h\u03c1\n have hmem2 : Nat.floor |\u03c1.1.im - t| = k := h\u03c1\n rw [farGRight, if_neg (fun h => hk (by\n have h1 : ((Nat.floor t + 1 : \u2115) : \u211d) \u2264 (k : \u211d) := by exact_mod_cast h.1\n have h2 : (Nat.floor t : \u211d) + 1 \u2264 (k : \u211d) := by\n have h3 : ((Nat.floor t + 1 : \u2115) : \u211d) = (Nat.floor t : \u211d) + 1 := by push_cast; ring\n rwa [h3] at h1\n have h4 : (Nat.floor t : \u211d) + 1 \u2264 |\u03c1.1.im - t| := by\n have h5 : (k : \u211d) \u2264 |\u03c1.1.im - t| := by\n have h6 := Nat.floor_le (abs_nonneg (\u03c1.1.im - t))\n rwa [hmem2] at h6\n linarith [h2, h5]\n exact h4 : Nat.floor t + 1 \u2264 |\u03c1.1.im - t|))]\n\n/-- loglog k \u2265 \u22120.37 for k \u2265 1 (the bridge nonnegativity input). -/\nlemma loglog_ge_neg_point37 {k : \u2115} (hk : 1 \u2264 k) :\n (-0.37 : \u211d) \u2264 Real.log (Real.log k) := by\n rcases eq_or_ne k 1 with rfl | hk1\n \u00b7 simp [Real.log_one, Real.log_zero]\n \u00b7 have hk2 : 2 \u2264 k := by omega\n have h1 : (0.693 : \u211d) \u2264 Real.log 2 := Real.log_two_gt_d9.le.trans (by norm_num)\n have h2 : (0.693 : \u211d) \u2264 Real.log k := by\n have h3 : Real.log 2 \u2264 Real.log k :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 2) (by exact_mod_cast hk2)\n linarith [h1, h3]\n have h4 : Real.log 0.693 \u2264 Real.log (Real.log k) :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 0.693) h2\n have h5 : (-0.37 : \u211d) \u2264 Real.log 0.693 := by\n have h6 : (1 / 0.693 : \u211d) \u2264 Real.exp 0.37 := by\n have h7 := Real.sum_le_exp_of_nonneg (show (0 : \u211d) \u2264 0.37 by norm_num) 5\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h7\n norm_num at h7\n have h8 : (1 / 0.693 : \u211d) \u2264 1.447671 := by norm_num\n linarith [h7, h8]\n have h7 : Real.log (1 / 0.693) \u2264 0.37 := by\n have h8 := Real.log_le_log (by norm_num : (0 : \u211d) < 1 / 0.693) h6\n rwa [Real.log_exp] at h8\n rw [Real.log_div (by norm_num : (1 : \u211d) \u2260 0) (by norm_num : (0.693 : \u211d) \u2260 0),\n Real.log_one] at h7\n linarith [h7]\n linarith [h4, h5]\n\n/-- The right-tail bridge is nonnegative for all k. -/\nlemma farGRightBridge_nonneg (k : \u2115) :\n (0 : \u211d) \u2264 0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9 := by\n by_cases hk0 : k = 0\n \u00b7 rw [hk0]\n simp only [Nat.cast_zero, Real.log_zero, Real.log_one, add_zero]\n norm_num\n \u00b7 have hk1 : 1 \u2264 k := by omega\n have h1 : (0 : \u211d) \u2264 Real.log k := Real.log_nonneg (by exact_mod_cast hk1 : (1 : \u211d) \u2264 (k : \u211d))\n have h2 := loglog_ge_neg_point37 hk1\n have h3 : (0 : \u211d) \u2264 (0.433 : \u211d) * (Real.log k + 0.833) := by\n apply mul_nonneg (by norm_num)\n linarith [h1]\n have h4 : (0.886 : \u211d) * ((-0.37 : \u211d) + 0.3475) \u2264 0.886 * (Real.log (Real.log k) + 0.3475) :=\n mul_le_mul_of_nonneg_left (by linarith [h2] : (-0.37 : \u211d) + 0.3475\n \u2264 Real.log (Real.log k) + 0.3475) (by norm_num)\n have h5 : (0.433 : \u211d) * 0.833 \u2264 0.433 * (Real.log k + 0.833) :=\n mul_le_mul_of_nonneg_left (by linarith [h1] : (0.833 : \u211d) \u2264 Real.log k + 0.833) (by norm_num)\n linarith [h3, h4, h5]\n\n/-- The right-tail majorant series (if-form on \u2115). -/\ndef farGRightMaj (t : \u211d) : \u2115 \u2192 \u211d := fun k =>\n if Nat.floor t + 1 \u2264 k then 4.5 * farW k * C0hat (2 * (k : \u211d) + 1) else 0\n\nlemma farGRightMaj_nonneg {t : \u211d} (k : \u2115) : (0 : \u211d) \u2264 farGRightMaj t k := by\n by_cases hk : Nat.floor t + 1 \u2264 k\n \u00b7 rw [farGRightMaj, if_pos hk]\n have h1 : (1 : \u211d) \u2264 (k : \u211d) + 1 + 1 := by\n have h2 : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith\n have h3 := two_le_C0hat h1\n have h4 : (0 : \u211d) \u2264 4.5 * farW k := by positivity\n exact mul_nonneg h4 (by linarith [h3])\n \u00b7 rw [farGRightMaj, if_neg hk]\n\n/-- The right-tail combo form (the brick decomposition target). -/\ndef farGRightMajCombo : \u2115 \u2192 \u211d := fun k =>\n 4.5 * (1 / (k : \u211d) ^ 2) * (0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9)\n\nlemma farGRightMajCombo_nonneg (k : \u2115) : (0 : \u211d) \u2264 farGRightMajCombo k := by\n rw [farGRightMajCombo]\n have h := farGRightBridge_nonneg k\n have h2 : (0 : \u211d) \u2264 4.5 * (1 / (k : \u211d) ^ 2) := by positivity\n exact mul_nonneg h2 h\n\n/-- The pointwise combo bound for the farGRightMaj. -/\nlemma farGRightMaj_le_combo {t : \u211d} (ht : 10 \u2264 t) (k : \u2115) :\n farGRightMaj t k \u2264 farGRightMajCombo k := by\n by_cases hk : Nat.floor t + 1 \u2264 k\n \u00b7 rw [farGRightMaj, if_pos hk, farGRightMajCombo]\n have hk11 : 11 \u2264 k := by\n have h1 : 10 \u2264 Nat.floor t := by\n have h2 := Nat.floor_mono (by norm_num : (10 : \u211d) \u2264 t)\n rwa [Nat.floor_ofNat] at h2\n omega\n have h1 := C0hat_two_mul_add_one_le hk11\n have h2 := farW_le_inv_sq (by omega : 1 \u2264 k)\n have hnn := farGRightBridge_nonneg k\n have h4 : 4.5 * farW k \u2264 4.5 * (1 / (k : \u211d) ^ 2) :=\n mul_le_mul_of_nonneg_left h2 (by norm_num : (0 : \u211d) \u2264 4.5)\n calc 4.5 * farW k * C0hat (2 * (k : \u211d) + 1)\n \u2264 (4.5 * (1 / (k : \u211d) ^ 2)) * (0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9) := by\n apply mul_le_mul h4 h1 hnn (by positivity : (0 : \u211d) \u2264 4.5 * (1 / (k : \u211d) ^ 2))\n \u00b7 rw [farGRightMaj, if_neg hk]\n exact farGRightMajCombo_nonneg k\n\n/-- The shifted LA\u2080-family for k \u2265 11 is summable. -/\nlemma tail11_inv_sq_summable :\n Summable (fun k : \u2115 => (1 : \u211d) / ((k : \u211d) + 11) ^ 2) := by\n have h := antitoneOn_one_div_sq.summable_of_integrableOn_Ioi\n integrableOn_one_div_sq (fun t ht => by\n have ht10 : (10 : \u211d) < t := ht\n positivity)\n have h2 := (summable_nat_add_iff (f := fun n : \u2115 => (1 : \u211d) / (n : \u211d) ^ 2) 11).mpr h\n refine h2.congr fun n => ?_\n push_cast\n ring_nf\n\n/-- The shifted LA\u2082-family for k \u2265 11 is summable. -/\nlemma tail11_loglog_div_sq_summable :\n Summable (fun k : \u2115 =>\n Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2) := by\n apply Summable.of_norm_bounded (tail11_log_div_sq_summable.mul_left (1 / Real.exp 1))\n intro k\n rw [Real.norm_eq_abs]\n rw [abs_of_nonneg (by\n have hk1 : (1 : \u211d) \u2264 Real.log ((k : \u211d) + 11) := by\n have h1 := log_eleven_ge\n have h2 : Real.log 11 \u2264 Real.log ((k : \u211d) + 11) :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 11) (by\n have h : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith)\n linarith [h1, h2]\n have h3 : (0 : \u211d) \u2264 Real.log (Real.log ((k : \u211d) + 11)) := Real.log_nonneg hk1\n positivity : (0 : \u211d) \u2264 Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2)]\n have hk1 : (1 : \u211d) < (k : \u211d) + 11 := by\n have h : (0 : \u211d) \u2264 (k : \u211d) := Nat.cast_nonneg k\n linarith\n have h4 := log_log_le_div_exp hk1\n have h5 : (0 : \u211d) \u2264 ((k : \u211d) + 11) ^ 2 := by positivity\n have h6 := div_le_div_of_nonneg_right h4 h5\n rw [mul_div_assoc] at h6\n exact h6\n\n/-- The shifted combo is summable (RW-brick families). -/\nlemma farGRightMajCombo_shift_summable :\n Summable (fun k : \u2115 => farGRightMajCombo (k + 11)) := by\n have hAB : Summable (fun k : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((k : \u211d) + 11) / ((k : \u211d) + 11) ^ 2)) :=\n (tail11_inv_sq_summable.mul_left _).add (tail11_log_div_sq_summable.mul_left _)\n have hABC : Summable (fun k : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((k : \u211d) + 11) / ((k : \u211d) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2)) :=\n hAB.add (tail11_loglog_div_sq_summable.mul_left _)\n have hsum := hABC.mul_left 4.5\n apply Summable.congr hsum\n intro k\n rw [farGRightMajCombo]\n have hcast : ((k + 11 : \u2115) : \u211d) = (k : \u211d) + 11 := by push_cast; ring\n rw [hcast]\n ring\n\nlemma farGRightMaj_summable {t : \u211d} (ht : 10 \u2264 t) : Summable (farGRightMaj t) := by\n apply (summable_nat_add_iff (f := farGRightMaj t) 11).mp\n apply Summable.of_norm_bounded farGRightMajCombo_shift_summable\n intro k\n rw [Real.norm_eq_abs, abs_of_nonneg (farGRightMaj_nonneg (k + 11))]\n exact farGRightMaj_le_combo ht (k + 11)\n\n/-- **The right-tail series bound**. -/\nlemma farGRightMaj_series_le {t : \u211d} (ht : 10 \u2264 t) :\n (\u2211' k : \u2115, farGRightMaj t k)\n \u2264 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n have hsplit : (\u2211' k : \u2115, farGRightMaj t k)\n = (\u2211 k \u2208 Finset.range 11, farGRightMaj t k) + \u2211' k : \u2115, farGRightMaj t (k + 11) :=\n ((farGRightMaj_summable ht).sum_add_tsum_nat_add 11).symm\n have hzero : \u2211 k \u2208 Finset.range 11, farGRightMaj t k = 0 := by\n apply Finset.sum_eq_zero\n intro k hk\n rw [Finset.mem_range] at hk\n rw [farGRightMaj, if_neg (by\n have h1 : 10 \u2264 Nat.floor t := by\n have h2 := Nat.floor_mono (by norm_num : (10 : \u211d) \u2264 t)\n rwa [Nat.floor_ofNat] at h2\n omega : \u00acNat.floor t + 1 \u2264 k)]\n have hle := Summable.tsum_le_tsum (fun k => farGRightMaj_le_combo ht (k + 11))\n (farGRightMaj_summable ht) farGRightMajCombo_shift_summable\n have hW0 := tail11_inv_sq_le\n have hW1 := tail11_log_div_sq_le\n have hW2 := tail11_loglog_div_sq_le\n have heval : (\u2211' k : \u2115,\n 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((k : \u211d) + 11) / ((k : \u211d) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((k : \u211d) + 11)) / ((k : \u211d) + 11) ^ 2)))\n \u2264 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * 0.1\n + 0.433 * 0.3303 + 0.886 * 0.1216) := by\n rw [tsum_mul_left]\n apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : \u211d) \u2264 4.5)\n have hdecomp : (\u2211' x : \u2115,\n ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2)))\n = (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (\u2211' x : \u2115, (1 / ((x : \u211d) + 11) ^ 2))\n + 0.433 * (\u2211' x : \u2115, (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2))\n + 0.886 * (\u2211' x : \u2115, (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2)) := by\n have e1 := Summable.tsum_add\n (f := fun x : \u2115 => (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2))\n (g := fun x : \u2115 => 0.886 * (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2))\n ((tail11_inv_sq_summable.mul_left _).add (tail11_log_div_sq_summable.mul_left _))\n (tail11_loglog_div_sq_summable.mul_left _)\n have e2 := Summable.tsum_add\n (f := fun x : \u2115 => (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2))\n (g := fun x : \u2115 => 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2))\n (tail11_inv_sq_summable.mul_left _) (tail11_log_div_sq_summable.mul_left _)\n rw [show (\u2211' x : \u2115,\n ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2)))\n = \u2211' x : \u2115, ((fun x : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)) x\n + (fun x : \u2115 => 0.886 * (Real.log (Real.log ((x : \u211d) + 11)) / ((x : \u211d) + 11) ^ 2)) x)\n from rfl]\n rw [e1]\n rw [show (\u2211' x : \u2115, (fun x : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)\n + 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)) x)\n = \u2211' x : \u2115, ((fun x : \u2115 =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : \u211d) + 11) ^ 2)) x\n + (fun x : \u2115 => 0.433 * (Real.log ((x : \u211d) + 11) / ((x : \u211d) + 11) ^ 2)) x)\n from rfl]\n rw [e2, tsum_mul_left, tsum_mul_left, tsum_mul_left]\n rw [hdecomp]\n have hle1 := mul_le_mul_of_nonneg_left hW0 (by positivity : (0 : \u211d) \u2264\n 0.433 * 0.833 + 0.886 * 0.3475 + 2.9)\n have hle2 := mul_le_mul_of_nonneg_left hW1 (by positivity : (0 : \u211d) \u2264 0.433)\n have hle3 := mul_le_mul_of_nonneg_left hW2 (by positivity : (0 : \u211d) \u2264 0.886)\n linarith [hle1, hle2, hle3]\n calc (\u2211' k : \u2115, farGRightMaj t k)\n = (\u2211 k \u2208 Finset.range 11, farGRightMaj t k) + \u2211' k : \u2115, farGRightMaj t (k + 11) := hsplit\n _ = 0 + \u2211' k : \u2115, farGRightMaj t (k + 11) := by rw [hzero]\n _ \u2264 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * 0.1\n + 0.433 * 0.3303 + 0.886 * 0.1216) := by linarith [hle, heval]\n _ = 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by ring\n\n/-- **The right-tail bound** (the ENNReal fiberwise assembly). -/\nlemma farGRight_le (hZC : ZeroCountProp) {t : \u211d} (ht : 10 \u2264 t) :\n \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, farGRight t \u03c1\n \u2264 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n have hC0 : (0 : \u211d) \u2264 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n positivity\n rw [\u2190 ENNReal.ofReal_le_ofReal_iff hC0]\n rw [ENNReal.ofReal_tsum_of_nonneg (fun \u03c1 => farGRight_nonneg t \u03c1)\n (farGRight_summable (by linarith : (0 : \u211d) \u2264 t))]\n rw [\u2190 ENNReal.tsum_fiberwise (fun \u03c1 => ENNReal.ofReal (farGRight t \u03c1))\n (fun \u03c1 => Nat.floor |\u03c1.1.im - t|)]\n have hper : \u2200 k : \u2115, \u2211' b : (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {k},\n ENNReal.ofReal (farGRight t b.1)\n \u2264 ENNReal.ofReal (farGRightMaj t k) := by\n intro k\n have h := farGRight_fiber_le hZC ht k\n rwa [farGRightMaj] at *\n calc \u2211' j : \u2115, \u2211' b : (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.floor |\u03c1.1.im - t|) \u207b\u00b9' {j},\n ENNReal.ofReal (farGRight t b.1)\n \u2264 \u2211' j : \u2115, ENNReal.ofReal (farGRightMaj t j) := ENNReal.tsum_le_tsum hper\n _ = ENNReal.ofReal (\u2211' j : \u2115, farGRightMaj t j) := by\n rw [ENNReal.ofReal_tsum_of_nonneg (fun k => farGRightMaj_nonneg k)\n (farGRightMaj_summable ht)]\n _ \u2264 ENNReal.ofReal (4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1)) :=\n ENNReal.ofReal_le_ofReal (farGRightMaj_series_le ht)\n\nend NguyenRH1\n\nend'''\n\nanchor = \"end NguyenRH1\\n\\nend\"\nassert src.count(anchor) == 1\nsrc = src.replace(anchor, section18)\nopen(p, 'w', encoding='utf-8').write(src)\nprint(\"inserted section 18\")\n",
"structuredPatch": [],
"originalFile": null
}
raw content_json (database row)
[{"type":"thinking","thinking":"Now I have the exact ending. Let me write §18 via a python insertion (avoiding the Edit-tool stale-read problem and letting me fix the placeholder). I'll write the section to a temp file and insert before `end NguyenRH1\\n\\nend`.\n\nKey fixes from the draft:\n1. Add `farGRightMaj_nonneg {t} (k) : 0 ≤ farGRightMaj t k` standalone.\n2. Add `farGRightMaj_summable {t} (ht : 10 ≤ t) : Summable (farGRightMaj t)` standalone (the hsumm body from series_le), and make series_le use it.\n3. farGRight_le's ofReal_tsum uses both.","signature":""},{"type":"text","text":"Writing §18 via python insertion with the summability lemmas properly factored."},{"type":"tool_use","id":"Write_227","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\insert_s18.py","content":"p = 'NguyenRH1/LiTightR.lean'\nsrc = open(p, encoding='utf-8').read()\n\nsection18 = '''\n/-! ## 18. Piece 3j: the right-tail machine (γ > 2t) -/\n\n/-- The right-tail summand: farG restricted to tail zeros (x ≥ ⌊t⌋₊+1)\non the right side (γ ≥ t, hence γ > 2t). -/\ndef farGRight (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℝ :=\n if (Nat.floor t + 1 ≤ |ρ.1.im - t| ∧ t ≤ ρ.1.im) then farG t ρ else 0\n\nlemma farGRight_nonneg (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : (0 : ℝ) ≤ farGRight t ρ := by\n by_cases h : (Nat.floor t + 1 ≤ |ρ.1.im - t| ∧ t ≤ ρ.1.im)\n · rw [farGRight, if_pos h]\n exact farG_nonneg t ρ\n · rw [farGRight, if_neg h]\n\nlemma farGRight_summable {t : ℝ} (ht : 0 ≤ t) : Summable (farGRight t) := by\n apply Summable.of_norm_bounded (farG_summable ht)\n intro ρ\n rw [Real.norm_eq_abs, abs_of_nonneg (farGRight_nonneg t ρ)]\n by_cases h : (Nat.floor t + 1 ≤ |ρ.1.im - t| ∧ t ≤ ρ.1.im)\n · rw [farGRight, if_pos h]\n · rw [farGRight, if_neg h]\n exact farG_nonneg t ρ\n\n/-- The per-element right-tail bound: farGRight ≤ 4.5·farW(⌊x⌋₊)·m. -/\nlemma farGRight_term_le {t : ℝ} (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n farGRight t ρ ≤ 4.5 * farW (Nat.floor |ρ.1.im - t|) * (zeroMult ρ.1 : ℝ) := by\n classical\n by_cases h : (Nat.floor t + 1 ≤ |ρ.1.im - t| ∧ t ≤ ρ.1.im)\n · rw [farGRight, if_pos h]\n have hx1 : (1 : ℝ) ≤ |ρ.1.im - t| := by\n have h1 : (1 : ℝ) ≤ (Nat.floor t : ℝ) + 1 := by\n have h2 : (0 : ℝ) ≤ (Nat.floor t : ℝ) := Nat.floor_nonneg\n linarith\n have h3 : (Nat.floor t : ℝ) + 1 ≤ |ρ.1.im - t| := by\n have h4 : ((Nat.floor t + 1 : ℕ) : ℝ) ≤ |ρ.1.im - t| := by exact_mod_cast h.1\n have h5 : ((Nat.floor t + 1 : ℕ) : ℝ) = (Nat.floor t : ℝ) + 1 := by push_cast; ring\n rwa [h5] at h4\n linarith [h1, h3]\n exact farG_le_farW_mul ρ hx1\n · rw [farGRight, if_neg h]\n positivity\n\n/-- The right-tail fiber {⌊x⌋₊ = k} is finite. -/\nlemma farGRight_fiber_finite {t : ℝ} (ht : 0 ≤ t) (k : ℕ) :\n ((fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {k} :\n Set {ρ : ℂ // IsNontrivialZero ρ}).Finite := by\n apply (finite_subtype_norm_lt (t + (k : ℝ) + 2)).subset\n intro ρ hρ\n show ‖ρ.1‖ < t + (k : ℝ) + 2\n have hmem : Nat.floor |ρ.1.im - t| = k := hρ\n have h1 : |ρ.1.im - t| < (k : ℝ) + 1 := by\n have h2 := Nat.lt_floor_add_one |ρ.1.im - t|\n rwa [hmem] at h2\n have hle : ‖ρ.1‖ ≤ |ρ.1.re| + |ρ.1.im| := Complex.norm_le_abs_re_add_abs_im _\n have hre : |ρ.1.re| ≤ 1 := by\n have h3 : 0 < ρ.1.re := ρ.2.2.1\n have h4 : ρ.1.re < 1 := ρ.2.2.2\n rw [abs_le]\n constructor <;> linarith\n have him : |ρ.1.im| ≤ t + |ρ.1.im - t| := by\n calc |ρ.1.im| = |ρ.1.im - t + t| := by rw [sub_add_cancel]\n _ ≤ |ρ.1.im - t| + |t| := abs_add_le _ _\n _ = |ρ.1.im - t| + t := by rw [abs_of_nonneg ht]\n _ = t + |ρ.1.im - t| := by ring\n linarith [hle, hre, him, h1]\n\n/-- **The per-fiber right-tail count**: the mult-weighted count of\nright-tail zeros with bucket k (⌊t⌋₊+1 ≤ k) is ≤ C0hat(2k+1). -/\nlemma farGRight_fiber_count (hZC : ZeroCountProp) {t : ℝ} (ht : 10 ≤ t)\n {k : ℕ} (hk : Nat.floor t + 1 ≤ k) :\n ∑ ρ ∈ (farGRight_fiber_finite (by linarith : (0 : ℝ) ≤ t) k).toFinset.filter\n (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => t ≤ ρ.1.im), (zeroMult ρ.1 : ℝ)\n ≤ C0hat (2 * (k : ℝ) + 1) := by\n classical\n set FS := (farGRight_fiber_finite (by linarith : (0 : ℝ) ≤ t) k).toFinset.filter\n (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => t ≤ ρ.1.im) with hFS\n have htk : (2 : ℝ) ≤ t + (k : ℝ) := by\n have h1 : (0 : ℝ) ≤ (k : ℝ) := Nat.cast_nonneg k\n linarith [ht, h1]\n have hcount : ((zeroWindow_finite (t + (k : ℝ))).toFinset.sum fun ρ => zeroMult ρ : ℝ)\n ≤ C0hat (t + (k : ℝ) + 1) := hZC (t + (k : ℝ)) htk\n have hmono : C0hat (t + (k : ℝ) + 1) ≤ C0hat (2 * (k : ℝ) + 1) := by\n apply C0hat_mono (by positivity : (1 : ℝ) ≤ t + (k : ℝ) + 1)\n have h1 : (Nat.floor t : ℝ) + 1 ≤ (k : ℝ) := by\n have h2 : ((Nat.floor t + 1 : ℕ) : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk\n have h3 : ((Nat.floor t + 1 : ℕ) : ℝ) = (Nat.floor t : ℝ) + 1 := by push_cast; ring\n rwa [h3] at h2\n have h4 : t ≤ (k : ℝ) := by\n have h5 : t ≤ (Nat.floor t : ℝ) + 1 := by\n have h6 := Nat.lt_floor_add_one t\n linarith [h6]\n linarith [h1, h5]\n linarith [h4]\n have hsub : FS.image (fun ρ => ρ.1) ⊆ (zeroWindow_finite (t + (k : ℝ))).toFinset := by\n intro z hz\n obtain ⟨ρ, hρ, rfl⟩ := Finset.mem_image.mp hz\n rw [hFS, Finset.mem_filter] at hρ\n obtain ⟨hmem, him⟩ := hρ\n rw [Set.Finite.mem_toFinset] at hmem\n have hmem2 : Nat.floor |ρ.1.im - t| = k := hmem\n have hxk : (k : ℝ) ≤ |ρ.1.im - t| := by\n have h1 := Nat.floor_le (abs_nonneg (ρ.1.im - t))\n rwa [hmem2] at h1\n have hxk1 : |ρ.1.im - t| < (k : ℝ) + 1 := by\n have h1 := Nat.lt_floor_add_one |ρ.1.im - t|\n rwa [hmem2] at h1\n have hx : |ρ.1.im - t| = ρ.1.im - t := abs_of_nonneg (by linarith [him])\n rw [Set.Finite.mem_toFinset]\n refine ⟨ρ.2, ?_, ?_⟩\n · rw [hx] at hxk\n linarith [hxk, him]\n · rw [hx] at hxk1\n linarith [hxk1, him]\n have hbridge : ∑ ρ ∈ FS, (zeroMult ρ.1 : ℝ)\n = ∑ ρ ∈ FS.image (fun ρ => ρ.1), (zeroMult ρ : ℝ) := by\n rw [Finset.sum_image (fun x _ y _ h => Subtype.ext h)]\n calc ∑ ρ ∈ FS, (zeroMult ρ.1 : ℝ)\n = ∑ z ∈ FS.image (fun ρ => ρ.1), (zeroMult z : ℝ) := hbridge\n _ ≤ ∑ z ∈ (zeroWindow_finite (t + (k : ℝ))).toFinset, (zeroMult z : ℝ) :=\n Finset.sum_le_sum_of_subset_of_nonneg hsub (fun z _ _ => Nat.cast_nonneg _)\n _ = (((zeroWindow_finite (t + (k : ℝ))).toFinset.sum fun ρ => zeroMult ρ) : ℝ) := rfl\n _ ≤ C0hat (t + (k : ℝ) + 1) := hcount\n _ ≤ C0hat (2 * (k : ℝ) + 1) := hmono\n\n/-- The per-fiber right-tail bound (ENNReal form). -/\nlemma farGRight_fiber_le (hZC : ZeroCountProp) {t : ℝ} (ht : 10 ≤ t) (k : ℕ) :\n ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {k},\n ENNReal.ofReal (farGRight t b.1)\n ≤ ENNReal.ofReal (if Nat.floor t + 1 ≤ k then 4.5 * farW k * C0hat (2 * (k : ℝ) + 1) else 0) := by\n classical\n have hfin : ((fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {k} :\n Set {ρ : ℂ // IsNontrivialZero ρ}).Finite := farGRight_fiber_finite (by linarith : (0 : ℝ) ≤ t) k\n have htsum : ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {k},\n ENNReal.ofReal (farGRight t b.1)\n = ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n ((fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {k}).indicator\n (fun ρ => ENNReal.ofReal (farGRight t ρ)) ρ :=\n tsum_subtype _ (fun ρ => ENNReal.ofReal (farGRight t ρ))\n rw [htsum]\n rw [tsum_eq_sum (s := hfin.toFinset) (fun ρ hρ => by\n apply Set.indicator_of_notMem\n rwa [Set.Finite.mem_toFinset] at hρ)]\n rw [Finset.sum_congr rfl (fun ρ hρ =>\n Set.indicator_of_mem (by rwa [Set.Finite.mem_toFinset] at hρ) _)]\n rw [← ENNReal.ofReal_sum_of_nonneg (fun ρ _ => farGRight_nonneg t ρ)]\n apply ENNReal.ofReal_le_ofReal\n by_cases hk : Nat.floor t + 1 ≤ k\n · rw [if_pos hk]\n rw [← Finset.sum_filter_add_sum_filter_not hfin.toFinset\n (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => t ≤ ρ.1.im) (farGRight t)]\n have hzero : ∑ ρ ∈ hfin.toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n ¬ t ≤ ρ.1.im), farGRight t ρ = 0 := by\n apply Finset.sum_eq_zero\n intro ρ hρ\n rw [Finset.mem_filter] at hρ\n rw [farGRight, if_neg (fun h => hρ.2 h.2)]\n rw [hzero, add_zero]\n calc ∑ ρ ∈ hfin.toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => t ≤ ρ.1.im),\n farGRight t ρ\n ≤ ∑ ρ ∈ hfin.toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => t ≤ ρ.1.im),\n (4.5 * farW k) * (zeroMult ρ.1 : ℝ) := by\n apply Finset.sum_le_sum\n intro ρ hρ\n have h1 := farGRight_term_le ρ\n rw [Finset.mem_filter] at hρ\n obtain ⟨hmem, _⟩ := hρ\n rw [Set.Finite.mem_toFinset] at hmem\n have hmem2 : Nat.floor |ρ.1.im - t| = k := hmem\n rw [hmem2] at h1\n exact h1\n _ = (4.5 * farW k) *\n ∑ ρ ∈ hfin.toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => t ≤ ρ.1.im),\n (zeroMult ρ.1 : ℝ) := by\n rw [Finset.mul_sum]\n _ ≤ (4.5 * farW k) * C0hat (2 * (k : ℝ) + 1) :=\n mul_le_mul_of_nonneg_left (farGRight_fiber_count hZC ht hk)\n (mul_nonneg (by norm_num : (0 : ℝ) ≤ 4.5) (farW_nonneg k))\n · rw [if_neg hk]\n apply le_of_eq\n apply Finset.sum_eq_zero\n intro ρ hρ\n rw [Set.Finite.mem_toFinset] at hρ\n have hmem2 : Nat.floor |ρ.1.im - t| = k := hρ\n rw [farGRight, if_neg (fun h => hk (by\n have h1 : ((Nat.floor t + 1 : ℕ) : ℝ) ≤ (k : ℝ) := by exact_mod_cast h.1\n have h2 : (Nat.floor t : ℝ) + 1 ≤ (k : ℝ) := by\n have h3 : ((Nat.floor t + 1 : ℕ) : ℝ) = (Nat.floor t : ℝ) + 1 := by push_cast; ring\n rwa [h3] at h1\n have h4 : (Nat.floor t : ℝ) + 1 ≤ |ρ.1.im - t| := by\n have h5 : (k : ℝ) ≤ |ρ.1.im - t| := by\n have h6 := Nat.floor_le (abs_nonneg (ρ.1.im - t))\n rwa [hmem2] at h6\n linarith [h2, h5]\n exact h4 : Nat.floor t + 1 ≤ |ρ.1.im - t|))]\n\n/-- loglog k ≥ −0.37 for k ≥ 1 (the bridge nonnegativity input). -/\nlemma loglog_ge_neg_point37 {k : ℕ} (hk : 1 ≤ k) :\n (-0.37 : ℝ) ≤ Real.log (Real.log k) := by\n rcases eq_or_ne k 1 with rfl | hk1\n · simp [Real.log_one, Real.log_zero]\n · have hk2 : 2 ≤ k := by omega\n have h1 : (0.693 : ℝ) ≤ Real.log 2 := Real.log_two_gt_d9.le.trans (by norm_num)\n have h2 : (0.693 : ℝ) ≤ Real.log k := by\n have h3 : Real.log 2 ≤ Real.log k :=\n Real.log_le_log (by norm_num : (0 : ℝ) < 2) (by exact_mod_cast hk2)\n linarith [h1, h3]\n have h4 : Real.log 0.693 ≤ Real.log (Real.log k) :=\n Real.log_le_log (by norm_num : (0 : ℝ) < 0.693) h2\n have h5 : (-0.37 : ℝ) ≤ Real.log 0.693 := by\n have h6 : (1 / 0.693 : ℝ) ≤ Real.exp 0.37 := by\n have h7 := Real.sum_le_exp_of_nonneg (show (0 : ℝ) ≤ 0.37 by norm_num) 5\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h7\n norm_num at h7\n have h8 : (1 / 0.693 : ℝ) ≤ 1.447671 := by norm_num\n linarith [h7, h8]\n have h7 : Real.log (1 / 0.693) ≤ 0.37 := by\n have h8 := Real.log_le_log (by norm_num : (0 : ℝ) < 1 / 0.693) h6\n rwa [Real.log_exp] at h8\n rw [Real.log_div (by norm_num : (1 : ℝ) ≠ 0) (by norm_num : (0.693 : ℝ) ≠ 0),\n Real.log_one] at h7\n linarith [h7]\n linarith [h4, h5]\n\n/-- The right-tail bridge is nonnegative for all k. -/\nlemma farGRightBridge_nonneg (k : ℕ) :\n (0 : ℝ) ≤ 0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9 := by\n by_cases hk0 : k = 0\n · rw [hk0]\n simp only [Nat.cast_zero, Real.log_zero, Real.log_one, add_zero]\n norm_num\n · have hk1 : 1 ≤ k := by omega\n have h1 : (0 : ℝ) ≤ Real.log k := Real.log_nonneg (by exact_mod_cast hk1 : (1 : ℝ) ≤ (k : ℝ))\n have h2 := loglog_ge_neg_point37 hk1\n have h3 : (0 : ℝ) ≤ (0.433 : ℝ) * (Real.log k + 0.833) := by\n apply mul_nonneg (by norm_num)\n linarith [h1]\n have h4 : (0.886 : ℝ) * ((-0.37 : ℝ) + 0.3475) ≤ 0.886 * (Real.log (Real.log k) + 0.3475) :=\n mul_le_mul_of_nonneg_left (by linarith [h2] : (-0.37 : ℝ) + 0.3475\n ≤ Real.log (Real.log k) + 0.3475) (by norm_num)\n have h5 : (0.433 : ℝ) * 0.833 ≤ 0.433 * (Real.log k + 0.833) :=\n mul_le_mul_of_nonneg_left (by linarith [h1] : (0.833 : ℝ) ≤ Real.log k + 0.833) (by norm_num)\n linarith [h3, h4, h5]\n\n/-- The right-tail majorant series (if-form on ℕ). -/\ndef farGRightMaj (t : ℝ) : ℕ → ℝ := fun k =>\n if Nat.floor t + 1 ≤ k then 4.5 * farW k * C0hat (2 * (k : ℝ) + 1) else 0\n\nlemma farGRightMaj_nonneg {t : ℝ} (k : ℕ) : (0 : ℝ) ≤ farGRightMaj t k := by\n by_cases hk : Nat.floor t + 1 ≤ k\n · rw [farGRightMaj, if_pos hk]\n have h1 : (1 : ℝ) ≤ (k : ℝ) + 1 + 1 := by\n have h2 : (0 : ℝ) ≤ (k : ℝ) := Nat.cast_nonneg k\n linarith\n have h3 := two_le_C0hat h1\n have h4 : (0 : ℝ) ≤ 4.5 * farW k := by positivity\n exact mul_nonneg h4 (by linarith [h3])\n · rw [farGRightMaj, if_neg hk]\n\n/-- The right-tail combo form (the brick decomposition target). -/\ndef farGRightMajCombo : ℕ → ℝ := fun k =>\n 4.5 * (1 / (k : ℝ) ^ 2) * (0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9)\n\nlemma farGRightMajCombo_nonneg (k : ℕ) : (0 : ℝ) ≤ farGRightMajCombo k := by\n rw [farGRightMajCombo]\n have h := farGRightBridge_nonneg k\n have h2 : (0 : ℝ) ≤ 4.5 * (1 / (k : ℝ) ^ 2) := by positivity\n exact mul_nonneg h2 h\n\n/-- The pointwise combo bound for the farGRightMaj. -/\nlemma farGRightMaj_le_combo {t : ℝ} (ht : 10 ≤ t) (k : ℕ) :\n farGRightMaj t k ≤ farGRightMajCombo k := by\n by_cases hk : Nat.floor t + 1 ≤ k\n · rw [farGRightMaj, if_pos hk, farGRightMajCombo]\n have hk11 : 11 ≤ k := by\n have h1 : 10 ≤ Nat.floor t := by\n have h2 := Nat.floor_mono (by norm_num : (10 : ℝ) ≤ t)\n rwa [Nat.floor_ofNat] at h2\n omega\n have h1 := C0hat_two_mul_add_one_le hk11\n have h2 := farW_le_inv_sq (by omega : 1 ≤ k)\n have hnn := farGRightBridge_nonneg k\n have h4 : 4.5 * farW k ≤ 4.5 * (1 / (k : ℝ) ^ 2) :=\n mul_le_mul_of_nonneg_left h2 (by norm_num : (0 : ℝ) ≤ 4.5)\n calc 4.5 * farW k * C0hat (2 * (k : ℝ) + 1)\n ≤ (4.5 * (1 / (k : ℝ) ^ 2)) * (0.433 * (Real.log k + 0.833)\n + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9) := by\n apply mul_le_mul h4 h1 hnn (by positivity : (0 : ℝ) ≤ 4.5 * (1 / (k : ℝ) ^ 2))\n · rw [farGRightMaj, if_neg hk]\n exact farGRightMajCombo_nonneg k\n\n/-- The shifted LA₀-family for k ≥ 11 is summable. -/\nlemma tail11_inv_sq_summable :\n Summable (fun k : ℕ => (1 : ℝ) / ((k : ℝ) + 11) ^ 2) := by\n have h := antitoneOn_one_div_sq.summable_of_integrableOn_Ioi\n integrableOn_one_div_sq (fun t ht => by\n have ht10 : (10 : ℝ) < t := ht\n positivity)\n have h2 := (summable_nat_add_iff (f := fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 2) 11).mpr h\n refine h2.congr fun n => ?_\n push_cast\n ring_nf\n\n/-- The shifted LA₂-family for k ≥ 11 is summable. -/\nlemma tail11_loglog_div_sq_summable :\n Summable (fun k : ℕ =>\n Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2) := by\n apply Summable.of_norm_bounded (tail11_log_div_sq_summable.mul_left (1 / Real.exp 1))\n intro k\n rw [Real.norm_eq_abs]\n rw [abs_of_nonneg (by\n have hk1 : (1 : ℝ) ≤ Real.log ((k : ℝ) + 11) := by\n have h1 := log_eleven_ge\n have h2 : Real.log 11 ≤ Real.log ((k : ℝ) + 11) :=\n Real.log_le_log (by norm_num : (0 : ℝ) < 11) (by\n have h : (0 : ℝ) ≤ (k : ℝ) := Nat.cast_nonneg k\n linarith)\n linarith [h1, h2]\n have h3 : (0 : ℝ) ≤ Real.log (Real.log ((k : ℝ) + 11)) := Real.log_nonneg hk1\n positivity : (0 : ℝ) ≤ Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2)]\n have hk1 : (1 : ℝ) < (k : ℝ) + 11 := by\n have h : (0 : ℝ) ≤ (k : ℝ) := Nat.cast_nonneg k\n linarith\n have h4 := log_log_le_div_exp hk1\n have h5 : (0 : ℝ) ≤ ((k : ℝ) + 11) ^ 2 := by positivity\n have h6 := div_le_div_of_nonneg_right h4 h5\n rw [mul_div_assoc] at h6\n exact h6\n\n/-- The shifted combo is summable (RW-brick families). -/\nlemma farGRightMajCombo_shift_summable :\n Summable (fun k : ℕ => farGRightMajCombo (k + 11)) := by\n have hAB : Summable (fun k : ℕ =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2)) :=\n (tail11_inv_sq_summable.mul_left _).add (tail11_log_div_sq_summable.mul_left _)\n have hABC : Summable (fun k : ℕ =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2)) :=\n hAB.add (tail11_loglog_div_sq_summable.mul_left _)\n have hsum := hABC.mul_left 4.5\n apply Summable.congr hsum\n intro k\n rw [farGRightMajCombo]\n have hcast : ((k + 11 : ℕ) : ℝ) = (k : ℝ) + 11 := by push_cast; ring\n rw [hcast]\n ring\n\nlemma farGRightMaj_summable {t : ℝ} (ht : 10 ≤ t) : Summable (farGRightMaj t) := by\n apply (summable_nat_add_iff (f := farGRightMaj t) 11).mp\n apply Summable.of_norm_bounded farGRightMajCombo_shift_summable\n intro k\n rw [Real.norm_eq_abs, abs_of_nonneg (farGRightMaj_nonneg (k + 11))]\n exact farGRightMaj_le_combo ht (k + 11)\n\n/-- **The right-tail series bound**. -/\nlemma farGRightMaj_series_le {t : ℝ} (ht : 10 ≤ t) :\n (∑' k : ℕ, farGRightMaj t k)\n ≤ 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n have hsplit : (∑' k : ℕ, farGRightMaj t k)\n = (∑ k ∈ Finset.range 11, farGRightMaj t k) + ∑' k : ℕ, farGRightMaj t (k + 11) :=\n ((farGRightMaj_summable ht).sum_add_tsum_nat_add 11).symm\n have hzero : ∑ k ∈ Finset.range 11, farGRightMaj t k = 0 := by\n apply Finset.sum_eq_zero\n intro k hk\n rw [Finset.mem_range] at hk\n rw [farGRightMaj, if_neg (by\n have h1 : 10 ≤ Nat.floor t := by\n have h2 := Nat.floor_mono (by norm_num : (10 : ℝ) ≤ t)\n rwa [Nat.floor_ofNat] at h2\n omega : ¬Nat.floor t + 1 ≤ k)]\n have hle := Summable.tsum_le_tsum (fun k => farGRightMaj_le_combo ht (k + 11))\n (farGRightMaj_summable ht) farGRightMajCombo_shift_summable\n have hW0 := tail11_inv_sq_le\n have hW1 := tail11_log_div_sq_le\n have hW2 := tail11_loglog_div_sq_le\n have heval : (∑' k : ℕ,\n 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((k : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2)))\n ≤ 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * 0.1\n + 0.433 * 0.3303 + 0.886 * 0.1216) := by\n rw [tsum_mul_left]\n apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : ℝ) ≤ 4.5)\n have hdecomp : (∑' x : ℕ,\n ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((x : ℝ) + 11)) / ((x : ℝ) + 11) ^ 2)))\n = (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (∑' x : ℕ, (1 / ((x : ℝ) + 11) ^ 2))\n + 0.433 * (∑' x : ℕ, (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2))\n + 0.886 * (∑' x : ℕ, (Real.log (Real.log ((x : ℝ) + 11)) / ((x : ℝ) + 11) ^ 2)) := by\n have e1 := Summable.tsum_add\n (f := fun x : ℕ => (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2))\n (g := fun x : ℕ => 0.886 * (Real.log (Real.log ((x : ℝ) + 11)) / ((x : ℝ) + 11) ^ 2))\n ((tail11_inv_sq_summable.mul_left _).add (tail11_log_div_sq_summable.mul_left _))\n (tail11_loglog_div_sq_summable.mul_left _)\n have e2 := Summable.tsum_add\n (f := fun x : ℕ => (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2))\n (g := fun x : ℕ => 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2))\n (tail11_inv_sq_summable.mul_left _) (tail11_log_div_sq_summable.mul_left _)\n rw [show (∑' x : ℕ,\n ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2)\n + 0.886 * (Real.log (Real.log ((x : ℝ) + 11)) / ((x : ℝ) + 11) ^ 2)))\n = ∑' x : ℕ, ((fun x : ℕ =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2)) x\n + (fun x : ℕ => 0.886 * (Real.log (Real.log ((x : ℝ) + 11)) / ((x : ℝ) + 11) ^ 2)) x)\n from rfl]\n rw [e1]\n rw [show (∑' x : ℕ, (fun x : ℕ =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2)\n + 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2)) x)\n = ∑' x : ℕ, ((fun x : ℕ =>\n (0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * (1 / ((x : ℝ) + 11) ^ 2)) x\n + (fun x : ℕ => 0.433 * (Real.log ((x : ℝ) + 11) / ((x : ℝ) + 11) ^ 2)) x)\n from rfl]\n rw [e2, tsum_mul_left, tsum_mul_left, tsum_mul_left]\n rw [hdecomp]\n have hle1 := mul_le_mul_of_nonneg_left hW0 (by positivity : (0 : ℝ) ≤\n 0.433 * 0.833 + 0.886 * 0.3475 + 2.9)\n have hle2 := mul_le_mul_of_nonneg_left hW1 (by positivity : (0 : ℝ) ≤ 0.433)\n have hle3 := mul_le_mul_of_nonneg_left hW2 (by positivity : (0 : ℝ) ≤ 0.886)\n linarith [hle1, hle2, hle3]\n calc (∑' k : ℕ, farGRightMaj t k)\n = (∑ k ∈ Finset.range 11, farGRightMaj t k) + ∑' k : ℕ, farGRightMaj t (k + 11) := hsplit\n _ = 0 + ∑' k : ℕ, farGRightMaj t (k + 11) := by rw [hzero]\n _ ≤ 4.5 * ((0.433 * 0.833 + 0.886 * 0.3475 + 2.9) * 0.1\n + 0.433 * 0.3303 + 0.886 * 0.1216) := by linarith [hle, heval]\n _ = 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by ring\n\n/-- **The right-tail bound** (the ENNReal fiberwise assembly). -/\nlemma farGRight_le (hZC : ZeroCountProp) {t : ℝ} (ht : 10 ≤ t) :\n ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, farGRight t ρ\n ≤ 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n have hC0 : (0 : ℝ) ≤ 4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n positivity\n rw [← ENNReal.ofReal_le_ofReal_iff hC0]\n rw [ENNReal.ofReal_tsum_of_nonneg (fun ρ => farGRight_nonneg t ρ)\n (farGRight_summable (by linarith : (0 : ℝ) ≤ t))]\n rw [← ENNReal.tsum_fiberwise (fun ρ => ENNReal.ofReal (farGRight t ρ))\n (fun ρ => Nat.floor |ρ.1.im - t|)]\n have hper : ∀ k : ℕ, ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {k},\n ENNReal.ofReal (farGRight t b.1)\n ≤ ENNReal.ofReal (farGRightMaj t k) := by\n intro k\n have h := farGRight_fiber_le hZC ht k\n rwa [farGRightMaj] at *\n calc ∑' j : ℕ, ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im - t|) ⁻¹' {j},\n ENNReal.ofReal (farGRight t b.1)\n ≤ ∑' j : ℕ, ENNReal.ofReal (farGRightMaj t j) := ENNReal.tsum_le_tsum hper\n _ = ENNReal.ofReal (∑' j : ℕ, farGRightMaj t j) := by\n rw [ENNReal.ofReal_tsum_of_nonneg (fun k => farGRightMaj_nonneg k)\n (farGRightMaj_summable ht)]\n _ ≤ ENNReal.ofReal (4.5 * (0.433 * (0.833 * 0.1 + 0.3303)\n + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1)) :=\n ENNReal.ofReal_le_ofReal (farGRightMaj_series_le ht)\n\nend NguyenRH1\n\nend'''\n\nanchor = \"end NguyenRH1\\n\\nend\"\nassert src.count(anchor) == 1\nsrc = src.replace(anchor, section18)\nopen(p, 'w', encoding='utf-8').write(src)\nprint(\"inserted section 18\")\n"},"extra_content":null}]