← Session 28 — ii′-5e: partial-fraction identity (zero series + F entire)
thinking (360 chars)
The heredoc broke — the content contains `'` (apostrophes in comments like "5e-iii's"). The quoted heredoc <<'EOF' should be fine with apostrophes... the issue: my content has `'` inside — with <<'EOF' quoting, apostrophes are fine; the problem might be the tool's handling. Let me use the Write/Edit tools instead. I'll use Edit to append after the last line.
Heredoc quoting issue — using Edit instead.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiFEntire.lean",
"old_string": " have h1 : -1 / (s / 2 + (n : \u2102)) / 2 = -1 / (s + 2 * (n : \u2102)) := by\n have e : s / 2 + (n : \u2102) = (s + 2 * (n : \u2102)) / 2 := by ring\n rw [e, neg_div, one_div_div]\n ring\n linear_combination h1",
"new_string": " have h1 : -1 / (s / 2 + (n : \u2102)) / 2 = -1 / (s + 2 * (n : \u2102)) := by\n have e : s / 2 + (n : \u2102) = (s + 2 * (n : \u2102)) / 2 := by ring\n rw [e, neg_div, one_div_div]\n ring\n linear_combination h1\n\n/-! ## 7. The witness at a nontrivial zero -/\n\n/-- The witness at a nontrivial zero \u03c1\u2080 (mult m): Fexpr agrees punctured\nwith W\u2080 \u2212 (seriesFun \u2212 m/(s\u2212\u03c1\u2080)) + 1/s + 1/(s\u22121) \u2212 (log \u03c0)/2 + \u03c8(s/2)/2,\nanalytic at \u03c1\u2080 (the NF witness + 5e-iii's polar subtraction; the\nelementary terms analytic since re \u03c1\u2080 \u2208 (0, 1)). -/\nlemma Fexpr_eventually_nontrivial {\u03c1\u2080 : \u2102} (h\u03c1 : IsNontrivialZero \u03c1\u2080) :\n \u2203 W : \u2102 \u2192 \u2102, AnalyticAt \u2102 W \u03c1\u2080 \u2227 \u2200\u1da0 s in \ud835\udcdd[\u2260] \u03c1\u2080, Fexpr s = W s := by\n have h\u03c11 : \u03c1\u2080 \u2260 1 := by\n intro h\n rw [h] at h\u03c1\n have hlt := h\u03c1.2.2\n rw [Complex.one_re] at hlt\n exact lt_irrefl 1 hlt\n obtain \u27e8W0, hW0, hW0eq\u27e9 := logDeriv_zeta_sub_mult_div_eventually h\u03c1.1 h\u03c11\n have hS : AnalyticAt \u2102 (fun s => seriesFun s - (zeroMult \u03c1\u2080 : \u2102) / (s - \u03c1\u2080)) \u03c1\u2080 :=\n seriesFun_sub_polar_analyticAt \u27e8\u03c1\u2080, h\u03c1\u27e9\n have hC : AnalyticAt \u2102 (fun s : \u2102 => 1 / s) \u03c1\u2080 := by\n apply AnalyticAt.div analyticAt_const analyticAt_id (by\n have hpos := h\u03c1.2.1\n intro hh\n rw [hh, Complex.zero_re] at hpos\n exact lt_irrefl 0 hpos)\n have hC1 : AnalyticAt \u2102 (fun s : \u2102 => 1 / (s - 1)) \u03c1\u2080 := by\n apply AnalyticAt.div analyticAt_const (g := fun s : \u2102 => s - 1) _ (sub_ne_zero.mpr h\u03c11)\n exact analyticAt_id.sub analyticAt_const\n have hD : AnalyticAt \u2102 (fun _ : \u2102 => (Real.log Real.pi : \u2102) / 2) \u03c1\u2080 := analyticAt_const\n have hE : AnalyticAt \u2102 (fun s => Complex.digamma (s / 2) / 2) \u03c1\u2080 := by\n apply analyticAt_digamma_div_two\n intro m h\n have h2 : \u03c1\u2080 = -2 * (m : \u2102) := by linear_combination 2 * h\n have h3 : \u03c1\u2080.re = -2 * (m : \u211d) := by rw [h2]; simp\n have h4 : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n linarith [h\u03c1.2.1]\n refine \u27e8fun s => W0 s - (seriesFun s - (zeroMult \u03c1\u2080 : \u2102) / (s - \u03c1\u2080)) + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2, ?_, ?_\u27e9\n \u00b7 exact ((((hW0.sub hS).add hC).add hC1).sub hD).add hE\n \u00b7 filter_upwards [hW0eq] with s hs\n show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2\n = W0 s - (seriesFun s - (zeroMult \u03c1\u2080 : \u2102) / (s - \u03c1\u2080)) + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2\n linear_combination hs\n\n/-! ## 8. The generic point -/\n\n/-- Fexpr is analytic at every good point: \u03b6 s \u2260 0 (the classification),\ns \u2260 0, 1, and s/2 off the digamma poles. -/\nlemma Fexpr_analyticAt_of_not_bad {s : \u2102} (hs : \u00ac badPoint s) :\n AnalyticAt \u2102 Fexpr s := by\n have hs0 : s \u2260 0 := fun h => hs (Or.inr (Or.inl h))\n have hs1 : s \u2260 1 := fun h => hs (Or.inr (Or.inr (Or.inl h)))\n have h\u03b6 : riemannZeta s \u2260 0 := by\n intro hz\n apply hs\n rcases zeta_zero_classification hz with h | h | \u27e8n, hn, h\u27e9\n \u00b7 exact Or.inl h\n \u00b7 exact Or.inr (Or.inl h)\n \u00b7 exact Or.inr (Or.inr (Or.inr \u27e8n, hn, h\u27e9))\n have hA : AnalyticAt \u2102 (logDeriv riemannZeta) s :=\n ((analyticAt_riemannZeta hs1).deriv).div (analyticAt_riemannZeta hs1) h\u03b6\n have hB : AnalyticAt \u2102 seriesFun s := seriesFun_analyticAt (fun h => hs (Or.inl h))\n have hC : AnalyticAt \u2102 (fun s : \u2102 => 1 / s) s := by\n apply AnalyticAt.div analyticAt_const analyticAt_id hs0\n have hC1 : AnalyticAt \u2102 (fun s : \u2102 => 1 / (s - 1)) s := by\n apply AnalyticAt.div analyticAt_const (g := fun s : \u2102 => s - 1) _ (sub_ne_zero.mpr hs1)\n exact analyticAt_id.sub analyticAt_const\n have hD : AnalyticAt \u2102 (fun _ : \u2102 => (Real.log Real.pi : \u2102) / 2) s := analyticAt_const\n have hE : AnalyticAt \u2102 (fun s => Complex.digamma (s / 2) / 2) s := by\n apply analyticAt_digamma_div_two\n intro m h\n apply hs\n have h2 : s = -2 * (m : \u2102) := by linear_combination 2 * h\n rcases Nat.eq_zero_or_pos m with hm0 | hm\n \u00b7 subst hm0\n simp at h2\n exact Or.inr (Or.inl h2)\n \u00b7 exact Or.inr (Or.inr (Or.inr \u27e8m, hm, h2\u27e9))\n show AnalyticAt \u2102 (fun s => logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2) s\n exact ((((hA.sub hB).add hC).add hC1).sub hD).add hE\n\n/-- Around a good point there is a ball of good points (the \u03b6 \u2260 0\ncontinuity ball \u2229 avoidance of {0, 1}). -/\nlemma exists_ball_good_of_not_bad {s : \u2102} (hs : \u00ac badPoint s) :\n \u2203 \u03b4 : \u211d, 0 < \u03b4 \u2227 \u2200 y \u2208 Metric.ball s \u03b4, \u00ac badPoint y := by\n have hs0 : s \u2260 0 := fun h => hs (Or.inr (Or.inl h))\n have hs1 : s \u2260 1 := fun h => hs (Or.inr (Or.inr (Or.inl h)))\n have h\u03b6 : riemannZeta s \u2260 0 := by\n intro hz\n apply hs\n rcases zeta_zero_classification hz with h | h | \u27e8n, hn, h\u27e9\n \u00b7 exact Or.inl h\n \u00b7 exact Or.inr (Or.inl h)\n \u00b7 exact Or.inr (Or.inr (Or.inr \u27e8n, hn, h\u27e9))\n obtain \u27e8\u03b5\u2081, h\u03b5\u2081, hball\u2081\u27e9 := Metric.eventually_nhds_iff_ball.mp\n ((analyticAt_riemannZeta hs1).continuousAt.eventually_ne h\u03b6)\n have hs0n : (0 : \u211d) < \u2016s\u2016 := norm_pos_iff.mpr hs0\n have hs1n : (0 : \u211d) < \u2016s - 1\u2016 := norm_pos_iff.mpr (sub_ne_zero.mpr hs1)\n refine \u27e8min \u03b5\u2081 (min (\u2016s\u2016 / 2) (\u2016s - 1\u2016 / 2)), lt_min h\u03b5\u2081 (lt_min (half_pos hs0n)\n (half_pos hs1n)), fun y hy => ?_\u27e9\n have h\u03b5\u2081y : dist y s < \u03b5\u2081 := lt_of_lt_of_le (Metric.mem_ball.mp hy) (min_le_left _ _)\n have h\u03b6y : riemannZeta y \u2260 0 := hball\u2081 y (Metric.mem_ball.mpr h\u03b5\u2081y)\n have h\u03b4s : dist y s < \u2016s\u2016 / 2 :=\n lt_of_lt_of_le (Metric.mem_ball.mp hy) ((min_le_right _ _).trans (min_le_left _ _))\n have h\u03b41 : dist y s < \u2016s - 1\u2016 / 2 :=\n lt_of_lt_of_le (Metric.mem_ball.mp hy) ((min_le_right _ _).trans (min_le_right _ _))\n have hy0 : y \u2260 0 := by\n intro h\n have h0 : dist (0 : \u2102) s = \u2016s\u2016 := by rw [Complex.dist_eq]; simp\n rw [h, h0] at h\u03b4s\n linarith\n have hy1 : y \u2260 1 := by\n intro h\n have h1 : dist (1 : \u2102) s = \u2016s - 1\u2016 := by\n rw [Complex.dist_eq, show (1 : \u2102) - s = -(s - 1) by ring, norm_neg]\n rw [h, h1] at h\u03b41\n linarith\n rintro (h | h | h | \u27e8n, hn, h\u27e9)\n \u00b7 exact h\u03b6y h.1\n \u00b7 exact hy0 h\n \u00b7 exact hy1 h\n \u00b7 rw [h] at h\u03b6y\n exact h\u03b6y (riemannZeta_neg_two_mul hn)\n\n/-! ## 9. The entire extension -/\n\n/-- The entire extension of Fexpr: the punctured-limit value. -/\ndef Gentire : \u2102 \u2192 \u2102 := fun s => limUnder (\ud835\udcdd[\u2260] s) Fexpr\n\n/-- At a good point, Gentire = Fexpr (continuity \u27f9 the punctured limit\nis the value). -/\nlemma gentire_eq_Fexpr {s : \u2102} (hs : \u00ac badPoint s) : Gentire s = Fexpr s := by\n haveI := nhdsNE_neBot s\n have hlim : Tendsto Fexpr (\ud835\udcdd[\u2260] s) (\ud835\udcdd (Fexpr s)) :=\n (Fexpr_analyticAt_of_not_bad hs).continuousAt.mono_left nhdsWithin_le_nhds\n exact tendsto_nhds_unique (tendsto_nhds_limUnder \u27e8Fexpr s, hlim\u27e9) hlim\n\n/-- At a bad point, Gentire agrees on a full neighborhood with the\nanalytic witness (punctured agreement + the value at the point by the\nlimUnder uniqueness). -/\nlemma gentire_eventually_eq_witness {s : \u2102} (hbad : badPoint s) :\n \u2203 W : \u2102 \u2192 \u2102, AnalyticAt \u2102 W s \u2227 Gentire =\u1da0[\ud835\udcdd s] W := by\n obtain \u27e8W, hW, hWeq\u27e9 : \u2203 W, AnalyticAt \u2102 W s \u2227 \u2200\u1da0 y in \ud835\udcdd[\u2260] s, Fexpr y = W y := by\n rcases hbad with h | h | h | \u27e8n, hn, h\u27e9\n \u00b7 exact Fexpr_eventually_nontrivial h\n \u00b7 subst h; exact Fexpr_eventually_zero\n \u00b7 subst h; exact Fexpr_eventually_one\n \u00b7 subst h; exact Fexpr_eventually_neg_two_mul hn\n obtain \u27e8\u03b4\u2082, h\u03b4\u2082, hgood\u27e9 : \u2203 \u03b4\u2082 > 0, \u2200 y \u2208 Metric.ball s \u03b4\u2082, y \u2260 s \u2192 \u00ac badPoint y := by\n rcases hbad with h | h | h | \u27e8n, hn, h\u27e9\n \u00b7 -- nontrivial s: isolation \u2229 the re \u2208 (0, 1) strip\n obtain \u27e8\u03b4, h\u03b4, hiso\u27e9 := nontrivialZero_isolated \u27e8s, h\u27e9\n have hr0 : (0 : \u211d) < s.re := h.2.1\n have hr1 : (0 : \u211d) < 1 - s.re := by linarith [h.2.2]\n refine \u27e8min \u03b4 (min s.re (1 - s.re)), lt_min h\u03b4 (lt_min hr0 hr1), fun y hy hyne hby => ?_\u27e9\n have hrey : (0 : \u211d) < y.re \u2227 y.re < 1 := by\n have hd := Metric.mem_ball.mp hy\n rw [Complex.dist_eq] at hd\n have hre_le : |y.re - s.re| \u2264 \u2016y - s\u2016 := by\n have h1 : (y - s).re = y.re - s.re := Complex.sub_re\n rw [\u2190 h1]\n exact Complex.abs_re_le_norm _\n have hlt : \u2016y - s\u2016 < min s.re (1 - s.re) := lt_of_lt_of_le hd (min_le_right _ _)\n rcases abs_lt.mp (lt_of_le_of_lt hre_le hlt) with \u27e8h1, h2\u27e9\n constructor <;> linarith\n rcases hby with hb | hb | hb | \u27e8m, hm, hb\u27e9\n \u00b7 have hle := hiso \u27e8y, hb\u27e9 (fun heq => hyne (Subtype.ext_iff.mp heq))\n have hd := Metric.mem_ball.mp hy\n rw [Complex.dist_eq] at hd\n linarith [lt_of_lt_of_le hd (min_le_left _ _), hle]\n \u00b7 rw [hb, Complex.zero_re] at hrey\n exact lt_irrefl 0 hrey.1\n \u00b7 rw [hb, Complex.one_re] at hrey\n exact lt_irrefl 1 hrey.2\n \u00b7 have hre : y.re = -2 * (m : \u211d) := by rw [hb]; simp\n have hm1 : (1 : \u211d) \u2264 (m : \u211d) := by exact_mod_cast hm\n linarith [hrey.1, hre, hm1]\n \u00b7 subst h\n -- s = 0: the \u03b6-continuity ball \u2229 ball(0, 1/2)\n obtain \u27e8\u03b5\u2081, h\u03b5\u2081, hball\u2081\u27e9 := Metric.eventually_nhds_iff_ball.mp\n ((analyticAt_riemannZeta (by norm_num : (0 : \u2102) \u2260 1)).continuousAt.eventually_ne\n (by rw [riemannZeta_zero]; norm_num))\n refine \u27e8min \u03b5\u2081 (1 / 2), lt_min h\u03b5\u2081 (by norm_num), fun y hy hyne hby => ?_\u27e9\n have h\u03b5\u2081y : y \u2208 Metric.ball 0 \u03b5\u2081 := Metric.ball_subset_ball (min_le_left _ _) hy\n have h\u03b6y : riemannZeta y \u2260 0 := hball\u2081 y h\u03b5\u2081y\n rcases hby with hb | hb | hb | \u27e8m, hm, hb\u27e9\n \u00b7 exact h\u03b6y hb.1\n \u00b7 exact hyne hb\n \u00b7 rw [hb] at hy\n have hd := Metric.mem_ball.mp (Metric.ball_subset_ball (min_le_right _ _) hy)\n rw [Complex.dist_eq] at hd\n norm_num at hd\n \u00b7 rw [hb] at h\u03b6y\n exact h\u03b6y (riemannZeta_neg_two_mul hm)\n \u00b7 subst h\n -- s = 1: the zetaA ball \u2229 ball(1, 1/2)\n obtain \u27e8\u03b5\u2081, h\u03b5\u2081, hball\u2081\u27e9 := Metric.eventually_nhds_iff_ball.mp zetaA_ne_zero_near_one\n refine \u27e8min \u03b5\u2081 (1 / 2), lt_min h\u03b5\u2081 (by norm_num), fun y hy hyne hby => ?_\u27e9\n have h\u03b5\u2081y : y \u2208 Metric.ball 1 \u03b5\u2081 := Metric.ball_subset_ball (min_le_left _ _) hy\n have hZA : zetaA y \u2260 0 := hball\u2081 y h\u03b5\u2081y\n have h\u03b6y : riemannZeta y \u2260 0 := by\n have e := zetaA_apply hyne\n intro hz\n rw [hz, mul_zero] at e\n exact hZA e\n rcases hby with hb | hb | hb | \u27e8m, hm, hb\u27e9\n \u00b7 exact h\u03b6y hb.1\n \u00b7 rw [hb] at hy\n have hd := Metric.mem_ball.mp (Metric.ball_subset_ball (min_le_right _ _) hy)\n rw [Complex.dist_eq] at hd\n norm_num at hd\n \u00b7 exact hyne hb\n \u00b7 rw [hb] at h\u03b6y\n exact h\u03b6y (riemannZeta_neg_two_mul hm)\n \u00b7 subst h\n -- s = \u22122n: ball(\u22122n, 1/2) is bad-point-free off the center\n refine \u27e81 / 2, by norm_num, fun y hy hyne hby => ?_\u27e9\n rcases hby with hb | hb | hb | \u27e8m, hm, hb\u27e9\n \u00b7 have hrey : y.re < 0 := by\n have hd := Metric.mem_ball.mp hy\n rw [Complex.dist_eq] at hd\n have hre_le : |y.re - (-2 * (n : \u211d))| \u2264 \u2016y - -2 * (n : \u2102)\u2016 := by\n have h1 : (y - -2 * (n : \u2102)).re = y.re - (-2 * (n : \u211d)) := by simp\n rw [\u2190 h1]\n exact Complex.abs_re_le_norm _\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n rcases abs_lt.mp (lt_of_le_of_lt hre_le hd) with \u27e8h1, h2\u27e9\n linarith\n have hpos := hb.2.1\n linarith\n \u00b7 have hd := Metric.mem_ball.mp hy\n rw [hb, Complex.dist_eq] at hd\n have hnorm : (2 : \u211d) \u2264 \u2016(0 : \u2102) - -2 * (n : \u2102)\u2016 := by\n have h6 : |((0 : \u2102) - -2 * (n : \u2102)).re| \u2264 \u2016(0 : \u2102) - -2 * (n : \u2102)\u2016 :=\n Complex.abs_re_le_norm _\n have hre : ((0 : \u2102) - -2 * (n : \u2102)).re = 2 * (n : \u211d) := by simp\n rw [hre] at h6\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n rw [abs_of_nonneg (by linarith : (0 : \u211d) \u2264 2 * (n : \u211d))] at h6\n linarith\n linarith [hd, hnorm]\n \u00b7 have hd := Metric.mem_ball.mp hy\n rw [hb, Complex.dist_eq] at hd\n have hnorm : (2 : \u211d) \u2264 \u2016(1 : \u2102) - -2 * (n : \u2102)\u2016 := by\n have h6 : |((1 : \u2102) - -2 * (n : \u2102)).re| \u2264 \u2016(1 : \u2102) - -2 * (n : \u2102)\u2016 :=\n Complex.abs_re_le_norm _\n have hre : ((1 : \u2102) - -2 * (n : \u2102)).re = 1 + 2 * (n : \u211d) := by simp\n rw [hre] at h6\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n rw [abs_of_nonneg (by linarith : (0 : \u211d) \u2264 1 + 2 * (n : \u211d))] at h6\n linarith\n linarith [hd, hnorm]\n \u00b7 -- y = \u22122m \u2260 \u22122n: distance 2|m \u2212 n| \u2265 2\n have hd := Metric.mem_ball.mp hy\n rw [hb, Complex.dist_eq] at hd\n have hmn : m \u2260 n := by\n intro hmn\n exact hyne (by rw [hb, hmn])\n have hnorm : (2 : \u211d) \u2264 \u2016(-2 * (m : \u2102)) - -2 * (n : \u2102)\u2016 := by\n have h6 : |((-2 * (m : \u2102)) - -2 * (n : \u2102)).re| \u2264\n \u2016(-2 * (m : \u2102)) - -2 * (n : \u2102)\u2016 := Complex.abs_re_le_norm _\n have hre : ((-2 * (m : \u2102)) - -2 * (n : \u2102)).re = 2 * ((n : \u211d) - (m : \u211d)) := by\n simp\n rw [hre] at h6\n have hmn' : (1 : \u211d) \u2264 |(n : \u211d) - (m : \u211d)| := by\n rcases lt_or_gt_of_ne hmn with hlt | hgt\n \u00b7 have h7 : (m : \u211d) + 1 \u2264 (n : \u211d) := by exact_mod_cast Nat.succ_le_of_lt hlt\n rw [abs_of_nonneg (by linarith)]\n linarith\n \u00b7 have h7 : (n : \u211d) + 1 \u2264 (m : \u211d) := by exact_mod_cast Nat.succ_le_of_lt hgt\n rw [abs_of_nonpos (by linarith)]\n linarith\n have h7 : |2 * ((n : \u211d) - (m : \u211d))| = 2 * |(n : \u211d) - (m : \u211d)| := by\n rw [abs_mul]\n norm_num\n rw [h7] at h6\n linarith [h6, hmn']\n linarith [hd, hnorm]\n -- assemble the full-neighborhood agreement\n have hWeqBall := hWeq\n rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff_ball] at hWeqBall\n obtain \u27e8\u03b5\u2081, h\u03b5\u2081, hWeqBall\u27e9 := hWeqBall\n refine \u27e8W, hW, ?_\u27e9\n rw [Metric.eventually_nhds_iff_ball]\n refine \u27e8min \u03b5\u2081 \u03b4\u2082, lt_min h\u03b5\u2081 h\u03b4\u2082, fun y hy => ?_\u27e9\n have h\u03b5\u2081y : y \u2208 Metric.ball s \u03b5\u2081 := Metric.ball_subset_ball (min_le_left _ _) hy\n have h\u03b4\u2082y : y \u2208 Metric.ball s \u03b4\u2082 := Metric.ball_subset_ball (min_le_right _ _) hy\n by_cases hye : y = s\n \u00b7 subst hye\n haveI := nhdsNE_neBot s\n have hWcont : Tendsto W (\ud835\udcdd[\u2260] s) (\ud835\udcdd (W s)) :=\n hW.continuousAt.mono_left nhdsWithin_le_nhds\n have hlim : Tendsto Fexpr (\ud835\udcdd[\u2260] s) (\ud835\udcdd (W s)) := Tendsto.congr' hWeq.symm hWcont\n show limUnder (\ud835\udcdd[\u2260] s) Fexpr = W s\n exact tendsto_nhds_unique (tendsto_nhds_limUnder \u27e8W s, hlim\u27e9) hlim\n \u00b7 have hygood : \u00ac badPoint y := hgood y h\u03b4\u2082y hye\n rw [gentire_eq_Fexpr hygood]\n exact hWeqBall y h\u03b5\u2081y hye\n\n/-- The ii\u2032-5e-iv capstone: Fexpr extends to an entire function agreeing\nwith it at every good point. -/\ntheorem gentire_analyticAt_and_eq :\n (\u2200 s : \u2102, AnalyticAt \u2102 Gentire s) \u2227 \u2200 s : \u2102, \u00ac badPoint s \u2192 Gentire s = Fexpr s := by\n refine \u27e8fun s => ?_, fun s hs => gentire_eq_Fexpr hs\u27e9\n by_cases hs : badPoint s\n \u00b7 obtain \u27e8W, hW, hWeq\u27e9 := gentire_eventually_eq_witness hs\n exact hW.congr hWeq.symm\n \u00b7 obtain \u27e8\u03b4, h\u03b4, hgood\u27e9 := exists_ball_good_of_not_bad hs\n exact (Fexpr_analyticAt_of_not_bad hs).congr (by\n rw [Metric.eventually_nhds_iff_ball]\n exact \u27e8\u03b4, h\u03b4, fun y hy => (gentire_eq_Fexpr (hgood y hy)).symm\u27e9)\n\nend NguyenRH1\n\nend"
}
raw content_json (database row)
[{"type":"thinking","thinking":"The heredoc broke — the content contains `'` (apostrophes in comments like \"5e-iii's\"). The quoted heredoc <<'EOF' should be fine with apostrophes... the issue: my content has `'` inside — with <<'EOF' quoting, apostrophes are fine; the problem might be the tool's handling. Let me use the Write/Edit tools instead. I'll use Edit to append after the last line.","signature":""},{"type":"text","text":"Heredoc quoting issue — using Edit instead."},{"type":"tool_use","id":"Edit_199","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiFEntire.lean","old_string":" have h1 : -1 / (s / 2 + (n : ℂ)) / 2 = -1 / (s + 2 * (n : ℂ)) := by\n have e : s / 2 + (n : ℂ) = (s + 2 * (n : ℂ)) / 2 := by ring\n rw [e, neg_div, one_div_div]\n ring\n linear_combination h1","new_string":" have h1 : -1 / (s / 2 + (n : ℂ)) / 2 = -1 / (s + 2 * (n : ℂ)) := by\n have e : s / 2 + (n : ℂ) = (s + 2 * (n : ℂ)) / 2 := by ring\n rw [e, neg_div, one_div_div]\n ring\n linear_combination h1\n\n/-! ## 7. The witness at a nontrivial zero -/\n\n/-- The witness at a nontrivial zero ρ₀ (mult m): Fexpr agrees punctured\nwith W₀ − (seriesFun − m/(s−ρ₀)) + 1/s + 1/(s−1) − (log π)/2 + ψ(s/2)/2,\nanalytic at ρ₀ (the NF witness + 5e-iii's polar subtraction; the\nelementary terms analytic since re ρ₀ ∈ (0, 1)). -/\nlemma Fexpr_eventually_nontrivial {ρ₀ : ℂ} (hρ : IsNontrivialZero ρ₀) :\n ∃ W : ℂ → ℂ, AnalyticAt ℂ W ρ₀ ∧ ∀ᶠ s in 𝓝[≠] ρ₀, Fexpr s = W s := by\n have hρ1 : ρ₀ ≠ 1 := by\n intro h\n rw [h] at hρ\n have hlt := hρ.2.2\n rw [Complex.one_re] at hlt\n exact lt_irrefl 1 hlt\n obtain ⟨W0, hW0, hW0eq⟩ := logDeriv_zeta_sub_mult_div_eventually hρ.1 hρ1\n have hS : AnalyticAt ℂ (fun s => seriesFun s - (zeroMult ρ₀ : ℂ) / (s - ρ₀)) ρ₀ :=\n seriesFun_sub_polar_analyticAt ⟨ρ₀, hρ⟩\n have hC : AnalyticAt ℂ (fun s : ℂ => 1 / s) ρ₀ := by\n apply AnalyticAt.div analyticAt_const analyticAt_id (by\n have hpos := hρ.2.1\n intro hh\n rw [hh, Complex.zero_re] at hpos\n exact lt_irrefl 0 hpos)\n have hC1 : AnalyticAt ℂ (fun s : ℂ => 1 / (s - 1)) ρ₀ := by\n apply AnalyticAt.div analyticAt_const (g := fun s : ℂ => s - 1) _ (sub_ne_zero.mpr hρ1)\n exact analyticAt_id.sub analyticAt_const\n have hD : AnalyticAt ℂ (fun _ : ℂ => (Real.log Real.pi : ℂ) / 2) ρ₀ := analyticAt_const\n have hE : AnalyticAt ℂ (fun s => Complex.digamma (s / 2) / 2) ρ₀ := by\n apply analyticAt_digamma_div_two\n intro m h\n have h2 : ρ₀ = -2 * (m : ℂ) := by linear_combination 2 * h\n have h3 : ρ₀.re = -2 * (m : ℝ) := by rw [h2]; simp\n have h4 : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m\n linarith [hρ.2.1]\n refine ⟨fun s => W0 s - (seriesFun s - (zeroMult ρ₀ : ℂ) / (s - ρ₀)) + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2, ?_, ?_⟩\n · exact ((((hW0.sub hS).add hC).add hC1).sub hD).add hE\n · filter_upwards [hW0eq] with s hs\n show logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2\n = W0 s - (seriesFun s - (zeroMult ρ₀ : ℂ) / (s - ρ₀)) + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2\n linear_combination hs\n\n/-! ## 8. The generic point -/\n\n/-- Fexpr is analytic at every good point: ζ s ≠ 0 (the classification),\ns ≠ 0, 1, and s/2 off the digamma poles. -/\nlemma Fexpr_analyticAt_of_not_bad {s : ℂ} (hs : ¬ badPoint s) :\n AnalyticAt ℂ Fexpr s := by\n have hs0 : s ≠ 0 := fun h => hs (Or.inr (Or.inl h))\n have hs1 : s ≠ 1 := fun h => hs (Or.inr (Or.inr (Or.inl h)))\n have hζ : riemannZeta s ≠ 0 := by\n intro hz\n apply hs\n rcases zeta_zero_classification hz with h | h | ⟨n, hn, h⟩\n · exact Or.inl h\n · exact Or.inr (Or.inl h)\n · exact Or.inr (Or.inr (Or.inr ⟨n, hn, h⟩))\n have hA : AnalyticAt ℂ (logDeriv riemannZeta) s :=\n ((analyticAt_riemannZeta hs1).deriv).div (analyticAt_riemannZeta hs1) hζ\n have hB : AnalyticAt ℂ seriesFun s := seriesFun_analyticAt (fun h => hs (Or.inl h))\n have hC : AnalyticAt ℂ (fun s : ℂ => 1 / s) s := by\n apply AnalyticAt.div analyticAt_const analyticAt_id hs0\n have hC1 : AnalyticAt ℂ (fun s : ℂ => 1 / (s - 1)) s := by\n apply AnalyticAt.div analyticAt_const (g := fun s : ℂ => s - 1) _ (sub_ne_zero.mpr hs1)\n exact analyticAt_id.sub analyticAt_const\n have hD : AnalyticAt ℂ (fun _ : ℂ => (Real.log Real.pi : ℂ) / 2) s := analyticAt_const\n have hE : AnalyticAt ℂ (fun s => Complex.digamma (s / 2) / 2) s := by\n apply analyticAt_digamma_div_two\n intro m h\n apply hs\n have h2 : s = -2 * (m : ℂ) := by linear_combination 2 * h\n rcases Nat.eq_zero_or_pos m with hm0 | hm\n · subst hm0\n simp at h2\n exact Or.inr (Or.inl h2)\n · exact Or.inr (Or.inr (Or.inr ⟨m, hm, h2⟩))\n show AnalyticAt ℂ (fun s => logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2) s\n exact ((((hA.sub hB).add hC).add hC1).sub hD).add hE\n\n/-- Around a good point there is a ball of good points (the ζ ≠ 0\ncontinuity ball ∩ avoidance of {0, 1}). -/\nlemma exists_ball_good_of_not_bad {s : ℂ} (hs : ¬ badPoint s) :\n ∃ δ : ℝ, 0 < δ ∧ ∀ y ∈ Metric.ball s δ, ¬ badPoint y := by\n have hs0 : s ≠ 0 := fun h => hs (Or.inr (Or.inl h))\n have hs1 : s ≠ 1 := fun h => hs (Or.inr (Or.inr (Or.inl h)))\n have hζ : riemannZeta s ≠ 0 := by\n intro hz\n apply hs\n rcases zeta_zero_classification hz with h | h | ⟨n, hn, h⟩\n · exact Or.inl h\n · exact Or.inr (Or.inl h)\n · exact Or.inr (Or.inr (Or.inr ⟨n, hn, h⟩))\n obtain ⟨ε₁, hε₁, hball₁⟩ := Metric.eventually_nhds_iff_ball.mp\n ((analyticAt_riemannZeta hs1).continuousAt.eventually_ne hζ)\n have hs0n : (0 : ℝ) < ‖s‖ := norm_pos_iff.mpr hs0\n have hs1n : (0 : ℝ) < ‖s - 1‖ := norm_pos_iff.mpr (sub_ne_zero.mpr hs1)\n refine ⟨min ε₁ (min (‖s‖ / 2) (‖s - 1‖ / 2)), lt_min hε₁ (lt_min (half_pos hs0n)\n (half_pos hs1n)), fun y hy => ?_⟩\n have hε₁y : dist y s < ε₁ := lt_of_lt_of_le (Metric.mem_ball.mp hy) (min_le_left _ _)\n have hζy : riemannZeta y ≠ 0 := hball₁ y (Metric.mem_ball.mpr hε₁y)\n have hδs : dist y s < ‖s‖ / 2 :=\n lt_of_lt_of_le (Metric.mem_ball.mp hy) ((min_le_right _ _).trans (min_le_left _ _))\n have hδ1 : dist y s < ‖s - 1‖ / 2 :=\n lt_of_lt_of_le (Metric.mem_ball.mp hy) ((min_le_right _ _).trans (min_le_right _ _))\n have hy0 : y ≠ 0 := by\n intro h\n have h0 : dist (0 : ℂ) s = ‖s‖ := by rw [Complex.dist_eq]; simp\n rw [h, h0] at hδs\n linarith\n have hy1 : y ≠ 1 := by\n intro h\n have h1 : dist (1 : ℂ) s = ‖s - 1‖ := by\n rw [Complex.dist_eq, show (1 : ℂ) - s = -(s - 1) by ring, norm_neg]\n rw [h, h1] at hδ1\n linarith\n rintro (h | h | h | ⟨n, hn, h⟩)\n · exact hζy h.1\n · exact hy0 h\n · exact hy1 h\n · rw [h] at hζy\n exact hζy (riemannZeta_neg_two_mul hn)\n\n/-! ## 9. The entire extension -/\n\n/-- The entire extension of Fexpr: the punctured-limit value. -/\ndef Gentire : ℂ → ℂ := fun s => limUnder (𝓝[≠] s) Fexpr\n\n/-- At a good point, Gentire = Fexpr (continuity ⟹ the punctured limit\nis the value). -/\nlemma gentire_eq_Fexpr {s : ℂ} (hs : ¬ badPoint s) : Gentire s = Fexpr s := by\n haveI := nhdsNE_neBot s\n have hlim : Tendsto Fexpr (𝓝[≠] s) (𝓝 (Fexpr s)) :=\n (Fexpr_analyticAt_of_not_bad hs).continuousAt.mono_left nhdsWithin_le_nhds\n exact tendsto_nhds_unique (tendsto_nhds_limUnder ⟨Fexpr s, hlim⟩) hlim\n\n/-- At a bad point, Gentire agrees on a full neighborhood with the\nanalytic witness (punctured agreement + the value at the point by the\nlimUnder uniqueness). -/\nlemma gentire_eventually_eq_witness {s : ℂ} (hbad : badPoint s) :\n ∃ W : ℂ → ℂ, AnalyticAt ℂ W s ∧ Gentire =ᶠ[𝓝 s] W := by\n obtain ⟨W, hW, hWeq⟩ : ∃ W, AnalyticAt ℂ W s ∧ ∀ᶠ y in 𝓝[≠] s, Fexpr y = W y := by\n rcases hbad with h | h | h | ⟨n, hn, h⟩\n · exact Fexpr_eventually_nontrivial h\n · subst h; exact Fexpr_eventually_zero\n · subst h; exact Fexpr_eventually_one\n · subst h; exact Fexpr_eventually_neg_two_mul hn\n obtain ⟨δ₂, hδ₂, hgood⟩ : ∃ δ₂ > 0, ∀ y ∈ Metric.ball s δ₂, y ≠ s → ¬ badPoint y := by\n rcases hbad with h | h | h | ⟨n, hn, h⟩\n · -- nontrivial s: isolation ∩ the re ∈ (0, 1) strip\n obtain ⟨δ, hδ, hiso⟩ := nontrivialZero_isolated ⟨s, h⟩\n have hr0 : (0 : ℝ) < s.re := h.2.1\n have hr1 : (0 : ℝ) < 1 - s.re := by linarith [h.2.2]\n refine ⟨min δ (min s.re (1 - s.re)), lt_min hδ (lt_min hr0 hr1), fun y hy hyne hby => ?_⟩\n have hrey : (0 : ℝ) < y.re ∧ y.re < 1 := by\n have hd := Metric.mem_ball.mp hy\n rw [Complex.dist_eq] at hd\n have hre_le : |y.re - s.re| ≤ ‖y - s‖ := by\n have h1 : (y - s).re = y.re - s.re := Complex.sub_re\n rw [← h1]\n exact Complex.abs_re_le_norm _\n have hlt : ‖y - s‖ < min s.re (1 - s.re) := lt_of_lt_of_le hd (min_le_right _ _)\n rcases abs_lt.mp (lt_of_le_of_lt hre_le hlt) with ⟨h1, h2⟩\n constructor <;> linarith\n rcases hby with hb | hb | hb | ⟨m, hm, hb⟩\n · have hle := hiso ⟨y, hb⟩ (fun heq => hyne (Subtype.ext_iff.mp heq))\n have hd := Metric.mem_ball.mp hy\n rw [Complex.dist_eq] at hd\n linarith [lt_of_lt_of_le hd (min_le_left _ _), hle]\n · rw [hb, Complex.zero_re] at hrey\n exact lt_irrefl 0 hrey.1\n · rw [hb, Complex.one_re] at hrey\n exact lt_irrefl 1 hrey.2\n · have hre : y.re = -2 * (m : ℝ) := by rw [hb]; simp\n have hm1 : (1 : ℝ) ≤ (m : ℝ) := by exact_mod_cast hm\n linarith [hrey.1, hre, hm1]\n · subst h\n -- s = 0: the ζ-continuity ball ∩ ball(0, 1/2)\n obtain ⟨ε₁, hε₁, hball₁⟩ := Metric.eventually_nhds_iff_ball.mp\n ((analyticAt_riemannZeta (by norm_num : (0 : ℂ) ≠ 1)).continuousAt.eventually_ne\n (by rw [riemannZeta_zero]; norm_num))\n refine ⟨min ε₁ (1 / 2), lt_min hε₁ (by norm_num), fun y hy hyne hby => ?_⟩\n have hε₁y : y ∈ Metric.ball 0 ε₁ := Metric.ball_subset_ball (min_le_left _ _) hy\n have hζy : riemannZeta y ≠ 0 := hball₁ y hε₁y\n rcases hby with hb | hb | hb | ⟨m, hm, hb⟩\n · exact hζy hb.1\n · exact hyne hb\n · rw [hb] at hy\n have hd := Metric.mem_ball.mp (Metric.ball_subset_ball (min_le_right _ _) hy)\n rw [Complex.dist_eq] at hd\n norm_num at hd\n · rw [hb] at hζy\n exact hζy (riemannZeta_neg_two_mul hm)\n · subst h\n -- s = 1: the zetaA ball ∩ ball(1, 1/2)\n obtain ⟨ε₁, hε₁, hball₁⟩ := Metric.eventually_nhds_iff_ball.mp zetaA_ne_zero_near_one\n refine ⟨min ε₁ (1 / 2), lt_min hε₁ (by norm_num), fun y hy hyne hby => ?_⟩\n have hε₁y : y ∈ Metric.ball 1 ε₁ := Metric.ball_subset_ball (min_le_left _ _) hy\n have hZA : zetaA y ≠ 0 := hball₁ y hε₁y\n have hζy : riemannZeta y ≠ 0 := by\n have e := zetaA_apply hyne\n intro hz\n rw [hz, mul_zero] at e\n exact hZA e\n rcases hby with hb | hb | hb | ⟨m, hm, hb⟩\n · exact hζy hb.1\n · rw [hb] at hy\n have hd := Metric.mem_ball.mp (Metric.ball_subset_ball (min_le_right _ _) hy)\n rw [Complex.dist_eq] at hd\n norm_num at hd\n · exact hyne hb\n · rw [hb] at hζy\n exact hζy (riemannZeta_neg_two_mul hm)\n · subst h\n -- s = −2n: ball(−2n, 1/2) is bad-point-free off the center\n refine ⟨1 / 2, by norm_num, fun y hy hyne hby => ?_⟩\n rcases hby with hb | hb | hb | ⟨m, hm, hb⟩\n · have hrey : y.re < 0 := by\n have hd := Metric.mem_ball.mp hy\n rw [Complex.dist_eq] at hd\n have hre_le : |y.re - (-2 * (n : ℝ))| ≤ ‖y - -2 * (n : ℂ)‖ := by\n have h1 : (y - -2 * (n : ℂ)).re = y.re - (-2 * (n : ℝ)) := by simp\n rw [← h1]\n exact Complex.abs_re_le_norm _\n have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n rcases abs_lt.mp (lt_of_le_of_lt hre_le hd) with ⟨h1, h2⟩\n linarith\n have hpos := hb.2.1\n linarith\n · have hd := Metric.mem_ball.mp hy\n rw [hb, Complex.dist_eq] at hd\n have hnorm : (2 : ℝ) ≤ ‖(0 : ℂ) - -2 * (n : ℂ)‖ := by\n have h6 : |((0 : ℂ) - -2 * (n : ℂ)).re| ≤ ‖(0 : ℂ) - -2 * (n : ℂ)‖ :=\n Complex.abs_re_le_norm _\n have hre : ((0 : ℂ) - -2 * (n : ℂ)).re = 2 * (n : ℝ) := by simp\n rw [hre] at h6\n have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n rw [abs_of_nonneg (by linarith : (0 : ℝ) ≤ 2 * (n : ℝ))] at h6\n linarith\n linarith [hd, hnorm]\n · have hd := Metric.mem_ball.mp hy\n rw [hb, Complex.dist_eq] at hd\n have hnorm : (2 : ℝ) ≤ ‖(1 : ℂ) - -2 * (n : ℂ)‖ := by\n have h6 : |((1 : ℂ) - -2 * (n : ℂ)).re| ≤ ‖(1 : ℂ) - -2 * (n : ℂ)‖ :=\n Complex.abs_re_le_norm _\n have hre : ((1 : ℂ) - -2 * (n : ℂ)).re = 1 + 2 * (n : ℝ) := by simp\n rw [hre] at h6\n have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n rw [abs_of_nonneg (by linarith : (0 : ℝ) ≤ 1 + 2 * (n : ℝ))] at h6\n linarith\n linarith [hd, hnorm]\n · -- y = −2m ≠ −2n: distance 2|m − n| ≥ 2\n have hd := Metric.mem_ball.mp hy\n rw [hb, Complex.dist_eq] at hd\n have hmn : m ≠ n := by\n intro hmn\n exact hyne (by rw [hb, hmn])\n have hnorm : (2 : ℝ) ≤ ‖(-2 * (m : ℂ)) - -2 * (n : ℂ)‖ := by\n have h6 : |((-2 * (m : ℂ)) - -2 * (n : ℂ)).re| ≤\n ‖(-2 * (m : ℂ)) - -2 * (n : ℂ)‖ := Complex.abs_re_le_norm _\n have hre : ((-2 * (m : ℂ)) - -2 * (n : ℂ)).re = 2 * ((n : ℝ) - (m : ℝ)) := by\n simp\n rw [hre] at h6\n have hmn' : (1 : ℝ) ≤ |(n : ℝ) - (m : ℝ)| := by\n rcases lt_or_gt_of_ne hmn with hlt | hgt\n · have h7 : (m : ℝ) + 1 ≤ (n : ℝ) := by exact_mod_cast Nat.succ_le_of_lt hlt\n rw [abs_of_nonneg (by linarith)]\n linarith\n · have h7 : (n : ℝ) + 1 ≤ (m : ℝ) := by exact_mod_cast Nat.succ_le_of_lt hgt\n rw [abs_of_nonpos (by linarith)]\n linarith\n have h7 : |2 * ((n : ℝ) - (m : ℝ))| = 2 * |(n : ℝ) - (m : ℝ)| := by\n rw [abs_mul]\n norm_num\n rw [h7] at h6\n linarith [h6, hmn']\n linarith [hd, hnorm]\n -- assemble the full-neighborhood agreement\n have hWeqBall := hWeq\n rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff_ball] at hWeqBall\n obtain ⟨ε₁, hε₁, hWeqBall⟩ := hWeqBall\n refine ⟨W, hW, ?_⟩\n rw [Metric.eventually_nhds_iff_ball]\n refine ⟨min ε₁ δ₂, lt_min hε₁ hδ₂, fun y hy => ?_⟩\n have hε₁y : y ∈ Metric.ball s ε₁ := Metric.ball_subset_ball (min_le_left _ _) hy\n have hδ₂y : y ∈ Metric.ball s δ₂ := Metric.ball_subset_ball (min_le_right _ _) hy\n by_cases hye : y = s\n · subst hye\n haveI := nhdsNE_neBot s\n have hWcont : Tendsto W (𝓝[≠] s) (𝓝 (W s)) :=\n hW.continuousAt.mono_left nhdsWithin_le_nhds\n have hlim : Tendsto Fexpr (𝓝[≠] s) (𝓝 (W s)) := Tendsto.congr' hWeq.symm hWcont\n show limUnder (𝓝[≠] s) Fexpr = W s\n exact tendsto_nhds_unique (tendsto_nhds_limUnder ⟨W s, hlim⟩) hlim\n · have hygood : ¬ badPoint y := hgood y hδ₂y hye\n rw [gentire_eq_Fexpr hygood]\n exact hWeqBall y hε₁y hye\n\n/-- The ii′-5e-iv capstone: Fexpr extends to an entire function agreeing\nwith it at every good point. -/\ntheorem gentire_analyticAt_and_eq :\n (∀ s : ℂ, AnalyticAt ℂ Gentire s) ∧ ∀ s : ℂ, ¬ badPoint s → Gentire s = Fexpr s := by\n refine ⟨fun s => ?_, fun s hs => gentire_eq_Fexpr hs⟩\n by_cases hs : badPoint s\n · obtain ⟨W, hW, hWeq⟩ := gentire_eventually_eq_witness hs\n exact hW.congr hWeq.symm\n · obtain ⟨δ, hδ, hgood⟩ := exists_ball_good_of_not_bad hs\n exact (Fexpr_analyticAt_of_not_bad hs).congr (by\n rw [Metric.eventually_nhds_iff_ball]\n exact ⟨δ, hδ, fun y hy => (gentire_eq_Fexpr (hgood y hy)).symm⟩)\n\nend NguyenRH1\n\nend"},"extra_content":null}]