← Session 10 — Website planning + local dashboard build
thinking (2628 chars)
The links in the card sections use `--accent` (#4f9cf9) on dark card background? Actually .tbl a uses accent color; but links inside .card outside tables — there's no general `a` styling, so default browser link color (dark blue) shows, hard to read on dark background. Fix: add global link styling for content area links.
Add to CSS:
```css
#content a { color: #7fb8ff; }
#content a:hover { color: #a8ccff; }
```
But careful not to override menu (menu has its own rules — menu is in #sidebar, so #content a won't affect it). .navbtn and .msg-open have own colors — more specific selectors win over #content a? .navbtn is class selector (0,1,0) vs #content a (1,0,1) — ID selector wins! #content a would override .navbtn color. To be safe, define:
```css
#content a { color: #7fb8ff; }
#content a:hover { color: #b3d4ff; }
```
and re-specify exceptions: .navbtn (already has color, need higher specificity: #content .navbtn or add !important... simpler: use `:where()` to keep specificity low: `#content a:where(:not(.navbtn):not(.msg-open))`. :where has zero specificity, so `a:where(...)` total specificity = (0,0,1) + element... `#content` counts though. Let me do: `#content a:not(.navbtn):not(.msg-open)` — specificity (1,2,1) vs .navbtn (0,1,0) → still wins for .navbtn? :not() adds the inner selector's specificity: (1 id, 2 classes, 1 element) > (0,1,0). So it would still override .navbtn. Hmm.
Cleanest: only style links that don't have a class:
```css
#content a:not([class]) { color: #8fbfff; }
#content a:not([class]):hover { color: #c0d9ff; text-decoration: underline; }
```
Specificity doesn't matter since others have classes. All plain content links (ledger links? those are in .tbl a — classless! .tbl a currently accent #4f9cf9. The #content a:not([class]) (1,1,1... actually :not([class]) is attribute selector = class-level: (1 id, 1 attr-class-level, 1 element) beats .tbl a (0,1,1). It would change table link color too — from #4f9cf9 to lighter #8fbfff. Is that OK? Table links were readable enough but slightly brighter is fine/better. Consistency good.
But .msg-open has class — keeps accent. .navbtn class — keeps. Topbar no links. Good.
Apply edit, restart server (CSS static file — served directly, no restart needed for static? Django runserver serves static via staticfiles finder each request — template changes need no restart either actually! Templates are loaded per-request in DEBUG (cached but invalidated). CSS/JS changes: static files served from disk each request. So NO restart needed for template/static changes. Only Python changes need restart. Just edit CSS and verify with curl.
The card-body links fall back to the browser default dark blue — only table links were styled. Adding a global content-link style (class-less links only, so buttons/nav keep their styling).
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\web\\dashboard\\static\\dashboard\\style.css",
"old_string": "h1 { font-size: 26px; margin: 10px 0 14px; }",
"new_string": "/* content links (class-less anchors in cards/body text) */\n#content a:not([class]) { color: #8fbfff; text-decoration: none; }\n#content a:not([class]):hover { color: #c4dcff; text-decoration: underline; }\n\nh1 { font-size: 26px; margin: 10px 0 14px; }"
}
result 2026-08-19 20:43:53Z → 2026-08-23 15:55:57Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiFEntire.lean",
"oldString": " exact (differentiableAt_const _).sub h2\n exact hdiff.analyticOnNhd Metric.isOpen_ball\n\n/-- The single-term split: for w \u2208 ball(\u2212n, 1/2), w \u2260 \u2212n,",
"newString": " exact (differentiableAt_const _).sub h2\n have hdiff2 : DifferentiableOn \u2102 (digammaSeriesPartSub n)\n (Metric.ball (-(n : \u2102)) (1 / 2)) := hdiff\n exact hdiff2.analyticOnNhd Metric.isOpen_ball\n\n/-- The single-term split: for w \u2208 ball(\u2212n, 1/2), w \u2260 \u2212n,",
"originalFile": "/-\nNguyenRH1/LiFEntire.lean \u2014 tier ii\u2032 sub-stage ii\u2032-5e-iv (D-068 \u00a74):\nthe partial-fraction difference function\n\n Fexpr s := logDeriv \u03b6 s \u2212 seriesFun s + 1/s + 1/(s\u22121) \u2212 (log \u03c0)/2 + \u03c8(s/2)/2\n\nis ENTIRE. The excluded set is\n\n badPoint s := IsNontrivialZero s \u2228 s = 0 \u2228 s = 1 \u2228 \u2203 n \u2265 1, s = \u22122n;\n\nat each bad point the principal parts cancel exactly (D-068 \u00a70's residue\nbookkeeping: +m vs +m at nontrivial zeros; \u22121 vs \u22121 at 1; 0 = \u22121+1 at 0;\n+1 vs +1 at \u22122n). Since Mathlib lacks a general removable-singularity\ntheorem, entirety is packaged via the punctured-limit extension\n\n Gentire s := limUnder (\ud835\udcdd[\u2260] s) Fexpr:\n\nat GOOD points Fexpr is analytic (hence the punctured limit is the\nvalue), at each BAD point an explicit analytic witness agrees with Fexpr\non a punctured neighbourhood (the principal-part splits), so Gentire is\neverywhere analytic and agrees with Fexpr at every good point\n(`gentire_analyticAt`, `gentire_eq_Fexpr`).\n\nThe witnesses:\n* nontrivial zero \u03c1\u2080: [logDeriv \u03b6 \u2212 m/(s\u2212\u03c1\u2080)] analytic by the order\n normal form (`logDeriv_zeta_sub_mult_div_eventually`, the LiSides NF\n block) + [seriesFun \u2212 m/(s\u2212\u03c1\u2080)] analytic by 5e-iii's\n `seriesFun_sub_polar_analyticAt`; the elementary terms analytic since\n re \u03c1\u2080 \u2208 (0, 1) avoids 0, 1, \u22122n.\n* s = 1: logDeriv \u03b6 + 1/(s\u22121) = logDeriv zetaA punctured (zetaA\n analytic, zetaA 1 = 1 \u2014 ii\u2032-1b).\n* s = 0: \u03c8(s/2)/2 + 1/s = \u2212\u03b3/2 + \u00bd\u00b7digammaSeriesPart(s/2) punctured\n (the digamma series, Zeta23 `DigammaSeries.digamma_series`; the series\n part analytic on ball(0, 1/2) by the M-test); logDeriv \u03b6 analytic at\n 0 (\u03b6(0) = \u22121/2 \u2260 0).\n* s = \u22122n: logDeriv \u03b6 \u2212 1/(s+2n) analytic (NF + `zeroMult_neg_two_mul`,\n session 026); \u03c8(s/2)/2 + 1/(s+2n) = \u00bd\u00b7H_n(s/2) punctured where H_n is\n the digamma series with the j = n\u22121 term dropped (analytic on\n ball(\u2212n, 1/2) by the eventually M-test).\n\nAlso proved: `zeta_zero_classification` (every zero of \u03b6 is nontrivial,\n0, or \u22122n \u2014 from Zeta23's `completedRiemannZeta_eq_zero_iff` +\n`Gamma\u211d_eq_zero_iff`) and `analyticAt_digamma` (\u03c8 analytic off\n{0} \u222a \u2212\u2115).\n\nArchive references: D-068 \u00a74, journal-028 (the series machinery),\njournal-017 (the NF block), journal-026 (zeroMult(\u22122n)).\n-/\nimport Mathlib\nimport Zeta23.Statement\nimport Zeta23.RvM.CountByIntegral\nimport Zeta23.GammaFacts.Series\nimport NguyenRH1.LiSeries\nimport NguyenRH1.LiTrivialZeros\nimport NguyenRH1.LiDigamma\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 0. The difference function and the excluded set -/\n\n/-- The partial-fraction difference function (D-068 \u00a70):\n\u03b6\u2032/\u03b6 \u2212 series + 1/s + 1/(s\u22121) \u2212 \u00bdlog \u03c0 + \u00bd\u03c8(s/2); entire after the\npunctured-limit extension (`Gentire`). -/\ndef Fexpr (s : \u2102) : \u2102 :=\n logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Complex.digamma (s / 2) / 2\n\n/-- The excluded set of the partial-fraction identity: the nontrivial\nzeros, 0, 1, and the trivial zeros \u22122n (n \u2265 1). -/\ndef badPoint (s : \u2102) : Prop :=\n IsNontrivialZero s \u2228 s = 0 \u2228 s = 1 \u2228 \u2203 n : \u2115, 1 \u2264 n \u2227 s = -2 * (n : \u2102)\n\n/-! ## 1. Digamma is analytic off {0} \u222a \u2212\u2115 -/\n\n/-- \u03c8 = logDeriv \u0393 is analytic at any w \u2209 {0} \u222a \u2212\u2115 (the finite-min ball\navoiding the poles; \u0393 analytic + nonzero there). -/\nlemma analyticAt_digamma {w : \u2102} (hw : \u2200 m : \u2115, w \u2260 -(m : \u2102)) :\n AnalyticAt \u2102 Complex.digamma w := by\n set M : \u2115 := \u2308\u2016w\u2016\u2309\u208a with hM\n have hMle : \u2016w\u2016 \u2264 M := Nat.le_ceil _\n set d : Finset \u211d := (Finset.range (M + 2)).image (fun m : \u2115 => \u2016w + (m : \u2102)\u2016) with hd\n have hdne : d.Nonempty := by\n refine \u27e8\u2016w\u2016, ?_\u27e9\n rw [hd]\n refine Finset.mem_image.mpr \u27e80, Finset.mem_range.mpr (by omega), ?_\u27e9\n simp\n have hdpos : \u2200 x \u2208 d, 0 < x := by\n intro x hx\n rw [hd] at hx\n obtain \u27e8m, -, rfl\u27e9 := Finset.mem_image.mp hx\n rw [norm_pos_iff]\n intro hz\n exact hw m (eq_neg_of_add_eq_zero_left hz)\n have hmin0 : 0 < d.min' hdne := hdpos _ (Finset.min'_mem _ _)\n set \u03b4 : \u211d := min (1 / 2) (d.min' hdne / 2) with h\u03b4\n have h\u03b40 : 0 < \u03b4 := lt_min (by norm_num) (half_pos hmin0)\n have h\u03b41 : \u03b4 \u2264 1 / 2 := min_le_left _ _\n have h\u03b42 : \u03b4 \u2264 d.min' hdne / 2 := min_le_right _ _\n -- every point of ball(w, \u03b4) avoids the poles\n have hball : \u2200 y \u2208 Metric.ball w \u03b4, \u2200 m : \u2115, y \u2260 -(m : \u2102) := by\n intro y hy m hye\n have hdist : \u2016y - w\u2016 < \u03b4 := by\n have := Metric.mem_ball.mp hy\n rwa [dist_eq_norm] at this\n by_cases hm : m < M + 2\n \u00b7 have hmem : \u2016w + (m : \u2102)\u2016 \u2208 d := by\n rw [hd]\n exact Finset.mem_image.mpr \u27e8m, Finset.mem_range.mpr hm, rfl\u27e9\n have hle : d.min' hdne \u2264 \u2016w + (m : \u2102)\u2016 := Finset.min'_le _ _ hmem\n have hnm : \u2016y + (m : \u2102)\u2016 = 0 := by rw [hye]; simp\n have hnorm : \u2016w + (m : \u2102)\u2016 \u2264 \u2016y + (m : \u2102)\u2016 + \u2016y - w\u2016 := by\n calc \u2016w + (m : \u2102)\u2016 = \u2016(y + (m : \u2102)) - (y - w)\u2016 := by congr 1; ring\n _ \u2264 \u2016y + (m : \u2102)\u2016 + \u2016y - w\u2016 := norm_sub_le _ _\n rw [hnm] at hnorm\n simp at hnorm\n linarith\n \u00b7 push Not at hm\n have hnm : y + (m : \u2102) = 0 := by rw [hye]; simp\n have hnorm : (m : \u211d) \u2264 \u2016y + (m : \u2102)\u2016 + \u2016y\u2016 := by\n calc (m : \u211d) = \u2016(m : \u2102)\u2016 := (RCLike.norm_natCast m).symm\n _ = \u2016(y + (m : \u2102)) - y\u2016 := by congr 1; ring\n _ \u2264 \u2016y + (m : \u2102)\u2016 + \u2016y\u2016 := norm_sub_le _ _\n rw [hnm] at hnorm\n simp at hnorm\n have hyw : \u2016y\u2016 \u2264 \u2016y - w\u2016 + \u2016w\u2016 := by\n calc \u2016y\u2016 = \u2016(y - w) + w\u2016 := by congr 1; ring\n _ \u2264 \u2016y - w\u2016 + \u2016w\u2016 := norm_add_le _ _\n have hmM : M + 2 \u2264 m := by omega\n have hmre : (M : \u211d) + 2 \u2264 (m : \u211d) := by exact_mod_cast hmM\n linarith [hMle, hdist, h\u03b41]\n -- \u0393 analytic on the ball\n have hGammaOn : DifferentiableOn \u2102 Complex.Gamma (Metric.ball w \u03b4) := by\n intro y hy\n exact Complex.differentiableAt_Gamma y (hball y hy) |>.differentiableWithinAt\n have hGammaAn : AnalyticOnNhd \u2102 Complex.Gamma (Metric.ball w \u03b4) :=\n hGammaOn.analyticOnNhd Metric.isOpen_ball\n have hAn : AnalyticOnNhd \u2102 (fun z => deriv Complex.Gamma z / Complex.Gamma z)\n (Metric.ball w \u03b4) := by\n intro y hy\n exact ((hGammaAn y hy).deriv).div (hGammaAn y hy)\n (Complex.Gamma_ne_zero (hball y hy))\n have heq : Complex.digamma = fun z => deriv Complex.Gamma z / Complex.Gamma z := by\n funext z\n rw [digamma_def, logDeriv_apply]\n rw [heq]\n exact hAn w (Metric.mem_ball_self h\u03b40)\n\n/-- \u03c8(s/2)/2 is analytic wherever s/2 avoids the poles. -/\nlemma analyticAt_digamma_div_two {s : \u2102} (h : \u2200 m : \u2115, s / 2 \u2260 -(m : \u2102)) :\n AnalyticAt \u2102 (fun s => Complex.digamma (s / 2) / 2) s := by\n have h1 : AnalyticAt \u2102 (fun s : \u2102 => s / 2) s := by\n apply AnalyticAt.div analyticAt_id analyticAt_const (by norm_num)\n have h2 : AnalyticAt \u2102 (Complex.digamma \u2218 fun s : \u2102 => s / 2) s :=\n AnalyticAt.comp (f := fun s : \u2102 => s / 2) (analyticAt_digamma h) h1\n apply AnalyticAt.div _ analyticAt_const (by norm_num : (2 : \u2102) \u2260 0)\n exact h2\n\n/-! ## 2. The zero classification -/\n\n/-- Every zero of \u03b6 is a nontrivial zero, 0, or a trivial zero \u22122n\n(from Zeta23's `completedRiemannZeta_eq_zero_iff` via the \u0393R-pole case\nsplit; `riemannZeta_ne_zero_of_one_le_re` excludes re \u2265 1). -/\nlemma zeta_zero_classification {s : \u2102} (hs : riemannZeta s = 0) :\n IsNontrivialZero s \u2228 s = 0 \u2228 \u2203 n : \u2115, 1 \u2264 n \u2227 s = -2 * (n : \u2102) := by\n by_cases h1 : 1 \u2264 s.re\n \u00b7 exact absurd hs (riemannZeta_ne_zero_of_one_le_re h1)\n \u00b7 push Not at h1\n by_cases h0 : 0 < s.re\n \u00b7 exact Or.inl \u27e8hs, h0, h1\u27e9\n \u00b7 push Not at h0\n by_cases hs0 : s = 0\n \u00b7 exact Or.inr (Or.inl hs0)\n \u00b7 by_cases hG : Complex.Gamma\u211d s = 0\n \u00b7 rw [Complex.Gamma\u211d_eq_zero_iff] at hG\n obtain \u27e8n, hn\u27e9 := hG\n rcases Nat.eq_zero_or_pos n with hn0 | hnpos\n \u00b7 subst hn0\n simp at hn\n exact absurd hn hs0\n \u00b7 exact Or.inr (Or.inr \u27e8n, hnpos, by rw [hn]; ring\u27e9)\n \u00b7 have h\u039b : completedRiemannZeta s = 0 := by\n rw [RvM.completedRiemannZeta_eq_Gamma\u211d_mul hs0 hG, hs, mul_zero]\n have hpos := (RvM.completedRiemannZeta_eq_zero_iff.mp h\u039b).2.1\n linarith\n\n/-! ## 3. The logDeriv normal-form witness at a zero -/\n\n/-- At a zero \u03c1\u2080 \u2260 1 of \u03b6, the subtraction of the polar term\nmult(\u03c1\u2080)/(s\u2212\u03c1\u2080) from logDeriv \u03b6 agrees punctured with an analytic\nfunction (the logDeriv of the NF factor h). Unified witness for the\nnontrivial and the trivial zeros (the LiSides NF block). -/\nlemma logDeriv_zeta_sub_mult_div_eventually {\u03c1\u2080 : \u2102} (_h\u03b6 : riemannZeta \u03c1\u2080 = 0)\n (h\u03c11 : \u03c1\u2080 \u2260 1) :\n \u2203 W : \u2102 \u2192 \u2102, AnalyticAt \u2102 W \u03c1\u2080 \u2227\n \u2200\u1da0 s in \ud835\udcdd[\u2260] \u03c1\u2080, logDeriv riemannZeta s - (zeroMult \u03c1\u2080 : \u2102) / (s - \u03c1\u2080) = W s := by\n have h\u03c1\u03b1 : AnalyticAt \u2102 riemannZeta \u03c1\u2080 := analyticAt_riemannZeta h\u03c11\n obtain \u27e8h, hh, hh0, hfh\u27e9 := h\u03c1\u03b1.analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne h\u03c11)\n refine \u27e8logDeriv h, hh.deriv.div hh hh0, ?_\u27e9\n filter_upwards [self_mem_nhdsWithin,\n mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds,\n mem_nhdsWithin_of_mem_nhds (hh.continuousAt.eventually_ne hh0),\n mem_nhdsWithin_of_mem_nhds hh.eventually_analyticAt] with s hs\u03c1 hfhs hhs hhas\n have hfhs' : riemannZeta =\u1da0[\ud835\udcdd s]\n (fun z => (z - \u03c1\u2080) ^ analyticOrderNatAt riemannZeta \u03c1\u2080 \u2022 h z) := hfhs\n have hs\u03c1' : s - \u03c1\u2080 \u2260 0 := sub_ne_zero.mpr hs\u03c1\n have hld : logDeriv riemannZeta s =\n (analyticOrderNatAt riemannZeta \u03c1\u2080 : \u2102) / (s - \u03c1\u2080) + logDeriv h s := by\n have e1 : logDeriv riemannZeta s =\n logDeriv (fun z => (z - \u03c1\u2080) ^ analyticOrderNatAt riemannZeta \u03c1\u2080 * h z) s := by\n simp only [logDeriv_apply, hfhs'.deriv_eq, hfhs'.self_of_nhds, smul_eq_mul]\n rw [e1, logDeriv_mul (f := fun z : \u2102 => (z - \u03c1\u2080) ^ analyticOrderNatAt riemannZeta \u03c1\u2080)\n (g := h) s (pow_ne_zero _ hs\u03c1') hhs (by fun_prop) hhas.differentiableAt]\n have e2 : logDeriv (fun z : \u2102 => (z - \u03c1\u2080) ^ analyticOrderNatAt riemannZeta \u03c1\u2080) s\n = (analyticOrderNatAt riemannZeta \u03c1\u2080 : \u2102) / (s - \u03c1\u2080) := by\n rw [show (fun z : \u2102 => (z - \u03c1\u2080) ^ analyticOrderNatAt riemannZeta \u03c1\u2080)\n = (fun x : \u2102 => x ^ analyticOrderNatAt riemannZeta \u03c1\u2080) \u2218 (fun z => z - \u03c1\u2080)\n from rfl,\n logDeriv_comp (by fun_prop) (by fun_prop), logDeriv_pow]\n simp\n rw [e2]\n have hmz : (zeroMult \u03c1\u2080 : \u2102) = (analyticOrderNatAt riemannZeta \u03c1\u2080 : \u2102) := rfl\n rw [hld, hmz]\n ring\n\n/-! ## 4. The witness at s = 1 -/\n\n/-- Near s = 1 (punctured): logDeriv \u03b6 s = logDeriv zetaA s \u2212 1/(s\u22121). -/\nlemma logDeriv_zeta_eq_logDeriv_zetaA_sub :\n \u2200\u1da0 s in \ud835\udcdd[\u2260] (1 : \u2102),\n logDeriv riemannZeta s = logDeriv zetaA s - 1 / (s - 1) := by\n filter_upwards [self_mem_nhdsWithin,\n mem_nhdsWithin_of_mem_nhds zetaA_ne_zero_near_one] with s hs1 hZA\n have hs1' : s - 1 \u2260 0 := sub_ne_zero.mpr hs1\n have h\u03b6 : riemannZeta s \u2260 0 := by\n have e := zetaA_apply hs1\n intro hz\n rw [hz, mul_zero] at e\n exact hZA e\n have hcong : zetaA =\u1da0[\ud835\udcdd s] (fun w : \u2102 => (w - 1) * riemannZeta w) := by\n filter_upwards [eventually_ne_nhds hs1] with z hz using zetaA_apply hz\n have hld : logDeriv zetaA s = 1 / (s - 1) + logDeriv riemannZeta s := by\n have e1 : logDeriv zetaA s = logDeriv (fun w : \u2102 => (w - 1) * riemannZeta w) s := by\n simp only [logDeriv_apply, hcong.deriv_eq, hcong.self_of_nhds]\n rw [e1, logDeriv_mul (f := fun w : \u2102 => w - 1) (g := riemannZeta) s hs1' h\u03b6\n (differentiableAt_id.sub (differentiableAt_const 1))\n (analyticAt_riemannZeta hs1).differentiableAt]\n have e2 : logDeriv (fun w : \u2102 => w - 1) s = 1 / (s - 1) := by\n have hd : deriv (fun w : \u2102 => w - 1) s = 1 :=\n ((hasDerivAt_id s).sub_const (1 : \u2102)).deriv\n rw [logDeriv_apply, hd]\n rw [e2]\n rw [hld]\n ring\n\n/-- The witness at s = 1: Fexpr agrees punctured with\nlogDeriv zetaA \u2212 seriesFun + 1/s \u2212 (log \u03c0)/2 + \u03c8(s/2)/2, analytic at 1. -/\nlemma Fexpr_eventually_one :\n \u2203 W : \u2102 \u2192 \u2102, AnalyticAt \u2102 W 1 \u2227 \u2200\u1da0 s in \ud835\udcdd[\u2260] (1 : \u2102), Fexpr s = W s := by\n have h1dig : \u2200 m : \u2115, (1 : \u2102) / 2 \u2260 -(m : \u2102) := by\n intro m h\n have hre := congrArg Complex.re h\n simp at hre\n have hm : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n linarith\n refine \u27e8fun s => logDeriv zetaA s - seriesFun s + 1 / s - (Real.log Real.pi : \u2102) / 2\n + Complex.digamma (s / 2) / 2, ?_, ?_\u27e9\n \u00b7 have hA : AnalyticAt \u2102 (logDeriv zetaA) 1 :=\n (zetaA_analyticAt_one.deriv).div zetaA_analyticAt_one (by rw [zetaA_one]; norm_num)\n have hB : AnalyticAt \u2102 seriesFun 1 := seriesFun_analyticAt (by\n intro h\n have hlt := h.2.2\n rw [Complex.one_re] at hlt\n exact lt_irrefl 1 hlt)\n have hC : AnalyticAt \u2102 (fun s : \u2102 => 1 / s) 1 :=\n analyticAt_const.div analyticAt_id (by norm_num)\n have hD : AnalyticAt \u2102 (fun s : \u2102 => (Real.log Real.pi : \u2102) / 2) 1 := analyticAt_const\n have hE : AnalyticAt \u2102 (fun s => Complex.digamma (s / 2) / 2) 1 :=\n analyticAt_digamma_div_two h1dig\n exact ((((hA.sub hB).add hC).sub hD).add hE)\n \u00b7 filter_upwards [logDeriv_zeta_eq_logDeriv_zetaA_sub] 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 = logDeriv zetaA s - seriesFun s + 1 / s - (Real.log Real.pi : \u2102) / 2\n + Complex.digamma (s / 2) / 2\n rw [hs]\n ring\n\n/-! ## 5. The digamma series part and the witness at s = 0 -/\n\n/-- The series part of the digamma partial-fraction expansion\n\u03a3'_j (1/(j+1) \u2212 1/(w+j+1)); analytic on ball(0, 1/2). -/\ndef digammaSeriesPart (w : \u2102) : \u2102 :=\n \u2211' j : \u2115, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))\n\n/-- Pole avoidance on ball(0, 1/2): w + j + 1 \u2260 0. -/\nlemma add_nat_add_one_ne_zero_of_mem_ball {w : \u2102} (hw : w \u2208 Metric.ball 0 (1 / 2)) (j : \u2115) :\n w + (j : \u2102) + 1 \u2260 0 := by\n have hwn : \u2016w\u2016 < 1 / 2 := by\n have h := Metric.mem_ball.mp hw\n rwa [dist_zero_right] at h\n intro h\n have h1 : (w + (j : \u2102) + 1).re = w.re + (j : \u211d) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n rw [h] at h1\n simp at h1\n have h2 : -\u2016w\u2016 \u2264 w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1\n have hj0 : (0 : \u211d) \u2264 (j : \u211d) := Nat.cast_nonneg j\n linarith\n\n/-- The digamma series part is analytic on ball(0, 1/2) (M-test,\n\u03a3 1/(j+1)\u00b2 majorant). -/\nlemma digammaSeriesPart_analyticOn :\n AnalyticOnNhd \u2102 digammaSeriesPart (Metric.ball 0 (1 / 2)) := by\n have hsum : Summable (fun j : \u2115 => (1 : \u211d) / ((j : \u211d) + 1) ^ 2) :=\n summable_div_add_one_sq 1\n have hu : HasSumUniformlyOn (fun (j : \u2115) => fun w : \u2102 => 1 / ((j : \u2102) + 1) - 1 / (w + j + 1))\n (fun w => \u2211' j : \u2115, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n (Metric.ball 0 (1 / 2)) := by\n apply HasSumUniformlyOn.of_norm_le_summable hsum\n intro j w hw\n have hwn : \u2016w\u2016 < 1 / 2 := by\n have h := Metric.mem_ball.mp hw\n rwa [dist_zero_right] at h\n have hj1 : (0 : \u211d) < (j : \u211d) + 1 := by positivity\n have hwj : w + (j : \u2102) + 1 \u2260 0 := add_nat_add_one_ne_zero_of_mem_ball hw j\n have hj0 : ((j : \u2102) + 1) \u2260 0 := Nat.cast_add_one_ne_zero j\n have halg : 1 / ((j : \u2102) + 1) - 1 / (w + j + 1)\n = w / (((j : \u2102) + 1) * (w + j + 1)) := by\n field_simp\n ring\n have hnorm1 : \u2016((j : \u2102) + 1)\u2016 = (j : \u211d) + 1 := by\n have e : ((j : \u2102) + 1) = ((j + 1 : \u2115) : \u2102) := by push_cast; ring\n rw [e, RCLike.norm_natCast, Nat.cast_add, Nat.cast_one]\n have hnorm2 : ((j : \u211d) + 1) / 2 \u2264 \u2016w + (j : \u2102) + 1\u2016 := by\n have h2 : (w + (j : \u2102) + 1).re \u2264 \u2016w + (j : \u2102) + 1\u2016 := Complex.re_le_norm _\n have h3 : (w + (j : \u2102) + 1).re = w.re + (j : \u211d) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n have h4 : -\u2016w\u2016 \u2264 w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1\n linarith\n rw [halg, norm_div, norm_mul, hnorm1]\n have hA2 : (0 : \u211d) < ((j : \u211d) + 1) ^ 2 := by positivity\n have hden0 : (0 : \u211d) < ((j : \u211d) + 1) * \u2016w + (j : \u2102) + 1\u2016 :=\n mul_pos hj1 (by linarith [hnorm2, hj1])\n rw [div_le_div_iff\u2080 hden0 hA2]\n nlinarith [hwn.le, hnorm2, hj1.le, sq_nonneg ((j : \u211d) + 1)]\n have htend : TendstoLocallyUniformlyOn\n (fun t : Finset \u2115 => fun w => \u2211 j \u2208 t, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n (fun w => \u2211' j : \u2115, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n atTop (Metric.ball 0 (1 / 2)) :=\n TendstoUniformlyOn.tendstoLocallyUniformlyOn\n (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu)\n have hdiff : DifferentiableOn \u2102 (fun w => \u2211' j : \u2115, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n (Metric.ball 0 (1 / 2)) := by\n apply htend.differentiableOn _ Metric.isOpen_ball\n apply Filter.Eventually.of_forall\n intro t w hw\n rw [show (fun w => \u2211 j \u2208 t, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n = \u2211 j \u2208 t, (fun w => 1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) from by\n funext w; simp [Finset.sum_apply]]\n apply DifferentiableAt.differentiableWithinAt\n apply DifferentiableAt.sum\n intro j _\n have hwj : w + (j : \u2102) + 1 \u2260 0 := add_nat_add_one_ne_zero_of_mem_ball hw j\n have h2 : DifferentiableAt \u2102 (fun w : \u2102 => 1 / (w + (j : \u2102) + 1)) w :=\n (differentiableAt_const (1 : \u2102)).div\n ((differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _))\n hwj\n exact (differentiableAt_const _).sub h2\n have hdiff2 : DifferentiableOn \u2102 digammaSeriesPart (Metric.ball 0 (1 / 2)) := hdiff\n exact hdiff2.analyticOnNhd Metric.isOpen_ball\n\n/-- The digamma series evaluation near 0 (punctured): for\nw \u2208 ball(0, 1/2), w \u2260 0. -/\nlemma digamma_eq_seriesPart_near_zero {w : \u2102}\n (hw : w \u2208 Metric.ball 0 (1 / 2)) (hw0 : w \u2260 0) :\n Complex.digamma w = -(Real.eulerMascheroniConstant : \u2102) - 1 / w + digammaSeriesPart w := by\n have hZ : w \u2208 Complex.integerComplement := by\n intro hk\n obtain \u27e8k, hk\u27e9 := hk\n -- w = (k : \u2124): |k| < 1/2 forces k = 0\n have hmem := Metric.mem_ball.mp hw\n rw [dist_zero_right] at hmem\n rw [\u2190 hk] at hmem\n have hk0 : (1 : \u211d) \u2264 \u2016(k : \u2102)\u2016 \u2228 k = 0 := by\n by_cases hkz : k = 0\n \u00b7 exact Or.inr hkz\n \u00b7 left\n have h1 : (1 : \u2124) \u2264 |k| := Int.one_le_abs hkz\n have h2 : \u2016(k : \u2102)\u2016 = |(k : \u211d)| := by\n rw [show ((k : \u2102)) = (((k : \u211d)) : \u2102) by push_cast; ring, Complex.norm_ofReal]\n rw [h2]\n have h3 : (1 : \u211d) \u2264 |(k : \u211d)| := by exact_mod_cast h1\n exact h3\n rcases hk0 with habs | hk0\n \u00b7 linarith\n \u00b7 exact hw0 (by rw [\u2190 hk, hk0]; simp)\n have h := Zeta23.DigammaSeries.digamma_series hZ\n rw [h]\n rfl\n\n/-- The witness at s = 0: Fexpr agrees punctured with\nlogDeriv \u03b6 \u2212 seriesFun + 1/(s\u22121) \u2212 (log \u03c0)/2 + (\u2212\u03b3 + digammaSeriesPart(s/2))/2,\nanalytic at 0. -/\nlemma Fexpr_eventually_zero :\n \u2203 W : \u2102 \u2192 \u2102, AnalyticAt \u2102 W 0 \u2227 \u2200\u1da0 s in \ud835\udcdd[\u2260] (0 : \u2102), Fexpr s = W s := by\n have hA : AnalyticAt \u2102 (logDeriv riemannZeta) 0 := by\n have hz : riemannZeta 0 \u2260 0 := by rw [riemannZeta_zero]; norm_num\n exact ((analyticAt_riemannZeta (by norm_num)).deriv).div\n (analyticAt_riemannZeta (by norm_num)) hz\n have hB : AnalyticAt \u2102 seriesFun 0 := seriesFun_analyticAt (by\n intro h\n have hpos := h.2.1\n rw [Complex.zero_re] at hpos\n exact lt_irrefl 0 hpos)\n have hC : AnalyticAt \u2102 (fun s : \u2102 => 1 / (s - 1)) 0 := by\n apply AnalyticAt.div analyticAt_const (g := fun s : \u2102 => s - 1) _ (by norm_num)\n exact analyticAt_id.sub analyticAt_const\n have hD : AnalyticAt \u2102 (fun _ : \u2102 => (Real.log Real.pi : \u2102) / 2) 0 := analyticAt_const\n have hE : AnalyticAt \u2102\n (fun s => (-(Real.eulerMascheroniConstant : \u2102) + digammaSeriesPart (s / 2)) / 2) 0 := by\n apply AnalyticAt.div _ analyticAt_const (by norm_num : (2 : \u2102) \u2260 0)\n apply AnalyticAt.add analyticAt_const\n have h1 : AnalyticAt \u2102 (fun s : \u2102 => s / 2) 0 := by\n apply AnalyticAt.div analyticAt_id analyticAt_const (by norm_num)\n have hdsp0 : AnalyticAt \u2102 digammaSeriesPart ((0 : \u2102) / 2) := by\n rw [zero_div]\n exact digammaSeriesPart_analyticOn 0 (Metric.mem_ball_self (by norm_num))\n exact AnalyticAt.comp (f := fun s : \u2102 => s / 2) hdsp0 h1\n refine \u27e8fun s => logDeriv riemannZeta s - seriesFun s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2\n + (-(Real.eulerMascheroniConstant : \u2102) + digammaSeriesPart (s / 2)) / 2, ?_, ?_\u27e9\n \u00b7 exact ((((hA.sub hB).add hC).sub hD).add hE)\n \u00b7 -- punctured agreement on ball(0, 1/2)\n rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff_ball]\n refine \u27e81 / 2, by norm_num, fun s hsball hsne => ?_\u27e9\n have hs0 : s \u2260 0 := hsne\n have hs2ball : s / 2 \u2208 Metric.ball 0 (1 / 2) := by\n rw [Metric.mem_ball, dist_zero_right] at hsball \u22a2\n rw [norm_div, RCLike.norm_ofNat]\n linarith\n have hs20 : s / 2 \u2260 0 := by\n intro h\n exact hs0 (by linear_combination 2 * h)\n have hdig := digamma_eq_seriesPart_near_zero hs2ball hs20\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 = logDeriv riemannZeta s - seriesFun s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2\n + (-(Real.eulerMascheroniConstant : \u2102) + digammaSeriesPart (s / 2)) / 2\n rw [hdig]\n ring\n\n/-! ## 6. The digamma series minus a pole term, and the witness at s = \u22122n -/\n\n/-- \u03b6(\u22122n) = 0 for n \u2265 1 (from `zeroMult_neg_two_mul`: the order is 1). -/\nlemma riemannZeta_neg_two_mul {n : \u2115} (hn : 1 \u2264 n) :\n riemannZeta (-2 * (n : \u2102)) = 0 := by\n by_contra h\n have hord := zeroMult_neg_two_mul n hn\n have hne1 : (-2 * (n : \u2102)) \u2260 1 := by\n intro hh\n have hre := congrArg Complex.re hh\n simp at hre\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n linarith\n have h0 : analyticOrderAt riemannZeta (-2 * (n : \u2102)) = 0 :=\n (analyticAt_riemannZeta hne1).analyticOrderAt_eq_zero.mpr h\n have hmz : zeroMult (-2 * (n : \u2102)) = analyticOrderNatAt riemannZeta (-2 * (n : \u2102)) := rfl\n rw [hmz] at hord\n simp only [analyticOrderNatAt] at hord\n rw [h0] at hord\n simp at hord\n\n/-- Pole avoidance on ball(\u2212n, 1/2) for j \u2260 n\u22121: w + j + 1 \u2260 0. -/\nlemma add_nat_add_one_ne_zero_of_mem_ball_neg {n : \u2115} (hn : 1 \u2264 n) {w : \u2102}\n (hw : w \u2208 Metric.ball (-(n : \u2102)) (1 / 2)) {j : \u2115} (hj : j \u2260 n - 1) :\n w + (j : \u2102) + 1 \u2260 0 := by\n intro h\n have h1 : w = -((j : \u2102) + 1) := by linear_combination h\n have h2 : dist w (-(n : \u2102)) < 1 / 2 := Metric.mem_ball.mp hw\n rw [h1, Complex.dist_eq] at h2\n have h3 : -((j : \u2102) + 1) - -(n : \u2102) = ((n : \u2102) - ((j : \u2102) + 1)) := by ring\n rw [h3] at h2\n have h4 : \u2016((n : \u2102) - ((j : \u2102) + 1))\u2016 = |(n : \u211d) - ((j : \u211d) + 1)| := by\n rw [show (n : \u2102) - ((j : \u2102) + 1) = (((n : \u211d) - ((j : \u211d) + 1)) : \u2102) by push_cast; ring,\n Complex.norm_ofReal]\n rw [h4] at h2\n have hne : n \u2260 j + 1 := by\n intro hc\n apply hj\n omega\n have h5 : (1 : \u211d) \u2264 |(n : \u211d) - ((j : \u211d) + 1)| := by\n rcases lt_or_gt_of_ne hne with hlt | hgt\n \u00b7 have h6 : (n : \u211d) + 1 \u2264 (j : \u211d) + 1 := by\n exact_mod_cast Nat.succ_le_of_lt hlt\n rw [abs_of_neg (by linarith : (n : \u211d) - ((j : \u211d) + 1) < 0)]\n linarith\n \u00b7 have h6 : (j : \u211d) + 1 + 1 \u2264 (n : \u211d) := by\n exact_mod_cast Nat.succ_le_of_lt hgt\n rw [abs_of_pos (by linarith : 0 < (n : \u211d) - ((j : \u211d) + 1))]\n linarith\n linarith\n\n/-- The digamma series with the j = n\u22121 term dropped; analytic on\nball(\u2212n, 1/2). -/\ndef digammaSeriesPartSub (n : \u2115) (w : \u2102) : \u2102 :=\n \u2211' j : \u2115, (if j = n - 1 then 0 else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n\n/-- The dropped-term series is analytic on ball(\u2212n, 1/2) (the eventually\nM-test with majorant (2n+1)/(j+1)\u00b2 for j \u2265 2n+1). -/\nlemma digammaSeriesPartSub_analyticOn {n : \u2115} (hn : 1 \u2264 n) :\n AnalyticOnNhd \u2102 (digammaSeriesPartSub n) (Metric.ball (-(n : \u2102)) (1 / 2)) := by\n have hsum : Summable (fun j : \u2115 => (2 * (n : \u211d) + 1) / ((j : \u211d) + 1) ^ 2) :=\n summable_div_add_one_sq _\n have hu : HasSumUniformlyOn\n (fun (j : \u2115) => fun w : \u2102 =>\n (if j = n - 1 then 0 else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n (fun w => \u2211' j : \u2115, (if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n (Metric.ball (-(n : \u2102)) (1 / 2)) := by\n apply HasSumUniformlyOn.of_norm_le_summable_eventually hsum\n rw [eventually_cofinite]\n apply (Set.finite_Iio (2 * n + 1)).subset\n intro j hj\n show j < 2 * n + 1\n by_contra hj2\n push Not at hj2\n apply hj\n intro w hw\n have hwn : \u2016w\u2016 < (n : \u211d) + 1 / 2 := by\n have h := Metric.mem_ball.mp hw\n rw [Complex.dist_eq] at h\n have htri : \u2016w\u2016 \u2264 \u2016w - -(n : \u2102)\u2016 + \u2016-(n : \u2102)\u2016 := by\n calc \u2016w\u2016 = \u2016(w - -(n : \u2102)) + -(n : \u2102)\u2016 := by congr 1; ring\n _ \u2264 _ := norm_add_le _ _\n have hnnorm : \u2016(-(n : \u2102))\u2016 = (n : \u211d) := by\n rw [norm_neg, RCLike.norm_natCast]\n linarith\n have hjne : j \u2260 n - 1 := by omega\n rw [if_neg hjne]\n have hwj : w + (j : \u2102) + 1 \u2260 0 :=\n add_nat_add_one_ne_zero_of_mem_ball_neg hn hw hjne\n have hj0 : ((j : \u2102) + 1) \u2260 0 := Nat.cast_add_one_ne_zero j\n have halg : 1 / ((j : \u2102) + 1) - 1 / (w + j + 1)\n = w / (((j : \u2102) + 1) * (w + j + 1)) := by\n field_simp\n ring\n have hnorm1 : \u2016((j : \u2102) + 1)\u2016 = (j : \u211d) + 1 := by\n have e : ((j : \u2102) + 1) = ((j + 1 : \u2115) : \u2102) := by push_cast; ring\n rw [e, RCLike.norm_natCast, Nat.cast_add, Nat.cast_one]\n have hj1 : (0 : \u211d) < (j : \u211d) + 1 := by positivity\n -- for j \u2265 2n+1: \u2016w + j + 1\u2016 \u2265 (j+1)/2\n have hnorm2 : ((j : \u211d) + 1) / 2 \u2264 \u2016w + (j : \u2102) + 1\u2016 := by\n have h2 : (w + (j : \u2102) + 1).re \u2264 \u2016w + (j : \u2102) + 1\u2016 := Complex.re_le_norm _\n have h3 : (w + (j : \u2102) + 1).re = w.re + (j : \u211d) + 1 := by\n simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n have h4 : -\u2016w\u2016 \u2264 w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1\n have hj2' : 2 * ((n : \u211d) + 1) \u2264 (j : \u211d) + 1 := by\n have h5 : 2 * n + 2 \u2264 j + 1 := by omega\n have h6 : (2 * n + 2 : \u2115) \u2264 j + 1 := h5\n have h7 : ((2 * n + 2 : \u2115) : \u211d) \u2264 ((j + 1 : \u2115) : \u211d) := by exact_mod_cast h6\n push_cast at h7\n linarith\n nlinarith [hwn]\n rw [halg, norm_div, norm_mul, hnorm1]\n have hA2 : (0 : \u211d) < ((j : \u211d) + 1) ^ 2 := by positivity\n have hden0 : (0 : \u211d) < ((j : \u211d) + 1) * \u2016w + (j : \u2102) + 1\u2016 :=\n mul_pos hj1 (by linarith [hnorm2, hj1])\n rw [div_le_div_iff\u2080 hden0 hA2]\n have hn0 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n nlinarith [hwn.le, hnorm2, hj1.le, sq_nonneg ((j : \u211d) + 1), hn0]\n have htend : TendstoLocallyUniformlyOn\n (fun t : Finset \u2115 => fun w =>\n \u2211 j \u2208 t, (if j = n - 1 then 0 else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n (fun w => \u2211' j : \u2115, (if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n atTop (Metric.ball (-(n : \u2102)) (1 / 2)) :=\n TendstoUniformlyOn.tendstoLocallyUniformlyOn\n (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp hu)\n have hdiff : DifferentiableOn \u2102 (fun w => \u2211' j : \u2115, (if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n (Metric.ball (-(n : \u2102)) (1 / 2)) := by\n apply htend.differentiableOn _ Metric.isOpen_ball\n apply Filter.Eventually.of_forall\n intro t w hw\n rw [show (fun w => \u2211 j \u2208 t, (if j = n - 1 then 0\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n = \u2211 j \u2208 t, (fun w => if j = n - 1 then 0\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))) from by\n funext w; simp [Finset.sum_apply]]\n apply DifferentiableAt.differentiableWithinAt\n apply DifferentiableAt.sum\n intro j _\n by_cases hj : j = n - 1\n \u00b7 show DifferentiableAt \u2102 (fun w => if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))) w\n simp only [if_pos hj]\n exact differentiableAt_const 0\n \u00b7 have hwj : w + (j : \u2102) + 1 \u2260 0 :=\n add_nat_add_one_ne_zero_of_mem_ball_neg hn hw hj\n show DifferentiableAt \u2102 (fun w => if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))) w\n simp only [if_neg hj]\n have h2 : DifferentiableAt \u2102 (fun w : \u2102 => 1 / (w + (j : \u2102) + 1)) w :=\n (differentiableAt_const (1 : \u2102)).div\n ((differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _))\n hwj\n exact (differentiableAt_const _).sub h2\n exact hdiff.analyticOnNhd Metric.isOpen_ball\n\n/-- The single-term split: for w \u2208 ball(\u2212n, 1/2), w \u2260 \u2212n,\ndigammaSeriesPart w = digammaSeriesPartSub n w + (1/n \u2212 1/(w+n)). -/\nlemma digammaSeriesPart_eq_sub_add_single {n : \u2115} (hn : 1 \u2264 n) {w : \u2102}\n (hw : w \u2208 Metric.ball (-(n : \u2102)) (1 / 2)) (hwn : w \u2260 -(n : \u2102)) :\n digammaSeriesPart w\n = digammaSeriesPartSub n w + (1 / (n : \u2102) - 1 / (w + (n : \u2102))) := by\n have hZ : w \u2208 Complex.integerComplement := by\n intro k hk\n -- w = (k:\u2124) with dist w (\u2212n) < 1/2 forces k = \u2212n\n have h2 : dist w (-(n : \u2102)) < 1 / 2 := Metric.mem_ball.mp hw\n rw [hk, Complex.dist_eq] at h2\n have h3 : (k : \u2102) - -(n : \u2102) = ((k + (n : \u2124)) : \u2102) := by push_cast; ring\n rw [h3, show (((k + (n : \u2124)) : \u2102)) = (((k + (n : \u2124) : \u2124) : \u211d) : \u2102) by push_cast; ring,\n Complex.norm_ofReal] at h2\n have h4 : |(k : \u211d) + (n : \u211d)| < 1 / 2 := by\n have : |(k + (n : \u2124) : \u211d)| < 1 / 2 := by\n have h5 : (((k + (n : \u2124) : \u2124) : \u211d) : \u2102) = ((k + (n : \u2124) : \u2124) : \u211d) := rfl\n -- h2 : \u2016\u2191(\u2191(k + \u2191n))\u2016 < 1/2 after the rws; normalize\n convert h2 using 2\n push_cast\n ring\n rwa [show ((k + (n : \u2124)) : \u211d) = (k : \u211d) + (n : \u211d) by push_cast; ring] at this\n have hk0 : k = -(n : \u2124) := by\n by_contra hkne\n have h1 : (1 : \u2124) \u2264 |k + (n : \u2124)| := Int.one_le_abs (by\n intro hh\n exact hkne (neg_eq_of_add_eq_zero_left (by linear_combination hh)))\n have h1r : (1 : \u211d) \u2264 |(k : \u211d) + (n : \u211d)| := by\n have e : |(k : \u211d) + (n : \u211d)| = (|k + (n : \u2124)| : \u211d) := by\n rw [show (k : \u211d) + (n : \u211d) = ((k + (n : \u2124) : \u2124) : \u211d) by push_cast; ring,\n RCLike.norm_natCast]\n rw [e]\n exact_mod_cast h1\n linarith\n exact hwn (by rw [hk, hk0]; push_cast; ring)\n have hfull : Summable (fun j : \u2115 => 1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) :=\n Zeta23.DigammaSeries.summable_digamma_series hZ\n have hsub : Summable (fun j : \u2115 => if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))) := by\n apply Summable.of_norm_bounded hfull.norm\n intro j\n by_cases hjj : j = n - 1 <;> simp [hjj]\n have hsingle : Summable (fun j : \u2115 => if j = n - 1\n then (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) else (0 : \u2102)) := by\n apply summable_of_hasFiniteSupport ((Set.finite_singleton (n - 1)).subset ?_)\n intro j hj\n rw [Function.mem_support, ne_eq] at hj\n by_contra h\n apply hj\n rw [if_neg (fun he => h (Set.mem_singleton_iff.mpr he))]\n have htsum : \u2211' j, (if j = n - 1 then (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) else (0 : \u2102))\n = 1 / (n : \u2102) - 1 / (w + (n : \u2102)) := by\n rw [tsum_eq_single (n - 1) (fun j hj => if_neg hj)]\n rw [if_pos rfl]\n congr 1\n \u00b7 rw [Nat.cast_sub hn, Nat.cast_one]\n ring\n \u00b7 congr 1\n rw [Nat.cast_sub hn, Nat.cast_one]\n ring\n calc digammaSeriesPart w\n = \u2211' j, (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) := rfl\n _ = \u2211' j, ((if j = n - 1 then (0 : \u2102) else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)))\n + (if j = n - 1 then (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) else (0 : \u2102))) := by\n apply tsum_congr\n intro j\n by_cases hjj : j = n - 1 <;> simp [hjj]\n _ = digammaSeriesPartSub n w\n + \u2211' j, (if j = n - 1 then (1 / ((j : \u2102) + 1) - 1 / (w + j + 1)) else (0 : \u2102)) :=\n Summable.tsum_add hsub hsingle\n _ = digammaSeriesPartSub n w + (1 / (n : \u2102) - 1 / (w + (n : \u2102))) := by rw [htsum]\n\n/-- H_n: digamma plus its pole term at \u2212n, minus the pole \u2014 analytic on\nball(\u2212n, 1/2). -/\ndef Hsub (n : \u2115) (w : \u2102) : \u2102 :=\n -(Real.eulerMascheroniConstant : \u2102) - 1 / w + digammaSeriesPartSub n w + 1 / (n : \u2102)\n\n/-- The punctured digamma split at \u2212n: digamma w = \u22121/(w+n) + H_n w. -/\nlemma digamma_eq_neg_inv_add_Hsub {n : \u2115} (hn : 1 \u2264 n) {w : \u2102}\n (hw : w \u2208 Metric.ball (-(n : \u2102)) (1 / 2)) (hwn : w \u2260 -(n : \u2102)) :\n Complex.digamma w = -1 / (w + (n : \u2102)) + Hsub n w := by\n have hZ : w \u2208 Complex.integerComplement := by\n intro k hk\n have h2 : dist w (-(n : \u2102)) < 1 / 2 := Metric.mem_ball.mp hw\n rw [hk, Complex.dist_eq] at h2\n have h3 : (k : \u2102) - -(n : \u2102) = ((k + (n : \u2124)) : \u2102) := by push_cast; ring\n rw [h3, show (((k + (n : \u2124)) : \u2102)) = (((k + (n : \u2124) : \u2124) : \u211d) : \u2102) by push_cast; ring,\n Complex.norm_ofReal] at h2\n have h4 : |(k : \u211d) + (n : \u211d)| < 1 / 2 := by\n have h5 : |(k + (n : \u2124) : \u211d)| < 1 / 2 := by\n convert h2 using 2\n push_cast\n ring\n rwa [show ((k + (n : \u2124)) : \u211d) = (k : \u211d) + (n : \u211d) by push_cast; ring] at h5\n have hk0 : k = -(n : \u2124) := by\n by_contra hkne\n have h1 : (1 : \u2124) \u2264 |k + (n : \u2124)| := Int.one_le_abs (by\n intro hh\n exact hkne (neg_eq_of_add_eq_zero_left (by linear_combination hh)))\n have h1r : (1 : \u211d) \u2264 |(k : \u211d) + (n : \u211d)| := by\n have e : |(k : \u211d) + (n : \u211d)| = (|k + (n : \u2124)| : \u211d) := by\n rw [show (k : \u211d) + (n : \u211d) = ((k + (n : \u2124) : \u2124) : \u211d) by push_cast; ring,\n RCLike.norm_natCast]\n rw [e]\n exact_mod_cast h1\n linarith\n exact hwn (by rw [hk, hk0]; push_cast; ring)\n have hdig := Zeta23.DigammaSeries.digamma_series hZ\n have hsplit := digammaSeriesPart_eq_sub_add_single hn hw hwn\n rw [hdig, Hsub, hsplit]\n ring\n\n/-- H_n is analytic at \u2212n. -/\nlemma Hsub_analyticAt {n : \u2115} (hn : 1 \u2264 n) :\n AnalyticAt \u2102 (Hsub n) (-(n : \u2102)) := by\n have hA : AnalyticAt \u2102 (fun _ : \u2102 => -(Real.eulerMascheroniConstant : \u2102)) _ := analyticAt_const\n have hB : AnalyticAt \u2102 (fun w : \u2102 => 1 / w) (-(n : \u2102)) := by\n apply AnalyticAt.div analyticAt_const analyticAt_id\n simp\n positivity\n have hC : AnalyticAt \u2102 (digammaSeriesPartSub n) (-(n : \u2102)) :=\n digammaSeriesPartSub_analyticOn hn (-(n : \u2102)) (Metric.mem_ball_self (by norm_num))\n have hD : AnalyticAt \u2102 (fun _ : \u2102 => 1 / (n : \u2102)) _ := analyticAt_const\n show AnalyticAt \u2102 (fun w => -(Real.eulerMascheroniConstant : \u2102) - 1 / w\n + digammaSeriesPartSub n w + 1 / (n : \u2102)) (-(n : \u2102))\n exact (((hA.sub hB).add hC).add hD)\n\n/-- The witness at s = \u22122n (n \u2265 1): Fexpr agrees punctured with\nWtriv \u2212 seriesFun + 1/s + 1/(s\u22121) \u2212 (log \u03c0)/2 + H_n(s/2)/2. -/\nlemma Fexpr_eventually_neg_two_mul {n : \u2115} (hn : 1 \u2264 n) :\n \u2203 W : \u2102 \u2192 \u2102, AnalyticAt \u2102 W (-2 * (n : \u2102)) \u2227\n \u2200\u1da0 s in \ud835\udcdd[\u2260] (-2 * (n : \u2102)), Fexpr s = W s := by\n have h\u03b6 := riemannZeta_neg_two_mul hn\n have hne1 : (-2 * (n : \u2102)) \u2260 1 := by\n intro hh\n have hre := congrArg Complex.re hh\n simp at hre\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n linarith\n obtain \u27e8Wtriv, hWtriv, hWtrivEq\u27e9 := logDeriv_zeta_sub_mult_div_eventually h\u03b6 hne1\n rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff_ball] at hWtrivEq\n obtain \u27e8\u03b5, h\u03b5, hWtrivEq\u27e9 := hWtrivEq\n have hmult : zeroMult (-2 * (n : \u2102)) = 1 := zeroMult_neg_two_mul n hn\n -- the pieces\n have hB : AnalyticAt \u2102 seriesFun (-2 * (n : \u2102)) := seriesFun_analyticAt (by\n intro h\n have hpos := h.2.1\n have hre : (-2 * (n : \u2102)).re = -2 * (n : \u211d) := by simp\n rw [hre] at hpos\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n linarith)\n have hC : AnalyticAt \u2102 (fun s : \u2102 => 1 / s) (-2 * (n : \u2102)) := by\n apply AnalyticAt.div analyticAt_const analyticAt_id\n simp\n positivity\n have hC1 : AnalyticAt \u2102 (fun s : \u2102 => 1 / (s - 1)) (-2 * (n : \u2102)) := by\n apply AnalyticAt.div analyticAt_const _ (by\n have hn1 : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n intro hh\n have hre := congrArg Complex.re hh\n simp at hre\n linarith)\n exact analyticAt_id.sub analyticAt_const\n have hD : AnalyticAt \u2102 (fun _ : \u2102 => (Real.log Real.pi : \u2102) / 2) _ := analyticAt_const\n have hE : AnalyticAt \u2102 (fun s => Hsub n (s / 2) / 2) (-2 * (n : \u2102)) := by\n apply AnalyticAt.div _ analyticAt_const (by norm_num : (2 : \u2102) \u2260 0)\n have h1 : AnalyticAt \u2102 (fun s : \u2102 => s / 2) (-2 * (n : \u2102)) := by\n apply AnalyticAt.div analyticAt_id analyticAt_const (by norm_num)\n have hval : (-2 * (n : \u2102)) / 2 = -(n : \u2102) := by ring\n rw [\u2190 hval]\n exact AnalyticAt.comp (f := fun s : \u2102 => s / 2) (Hsub_analyticAt hn) h1\n refine \u27e8fun s => Wtriv s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Hsub n (s / 2) / 2, ?_, ?_\u27e9\n \u00b7 exact ((((hWtriv.sub hB).add hC).add hC1).sub hD).add hE\n \u00b7 -- punctured agreement on ball(\u22122n, min 1 \u03b5) (then s/2 \u2208 ball(\u2212n, 1/2))\n rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff_ball]\n refine \u27e8min 1 \u03b5, lt_min (by norm_num) h\u03b5, fun s hsball hsne => ?_\u27e9\n have hs0 : s \u2260 -2 * (n : \u2102) := hsne\n have hsdist : dist s (-2 * (n : \u2102)) < 1 \u2227 dist s (-2 * (n : \u2102)) < \u03b5 := by\n have h := Metric.mem_ball.mp hsball\n constructor <;> linarith [h, min_le_left 1 \u03b5, min_le_right 1 \u03b5]\n have hs2ball : s / 2 \u2208 Metric.ball (-(n : \u2102)) (1 / 2) := by\n rw [Metric.mem_ball, Complex.dist_eq]\n have e : s / 2 - -(n : \u2102) = (s - -2 * (n : \u2102)) / 2 := by ring\n rw [e, norm_div, RCLike.norm_ofNat]\n have h := Metric.mem_ball.mp hsball\n rw [Complex.dist_eq] at h\n linarith [h, min_le_left 1 \u03b5]\n have hs20 : s / 2 \u2260 -(n : \u2102) := by\n intro h\n exact hs0 (by linear_combination 2 * h)\n have hdig := digamma_eq_neg_inv_add_Hsub hn hs2ball hs20\n -- logDeriv split: logDeriv \u03b6 s = Wtriv s + 1/(s + 2n)\n have hlog : logDeriv riemannZeta s = Wtriv s + 1 / (s + 2 * (n : \u2102)) := by\n have h3 := hWtrivEq s (Metric.mem_ball.mpr hsdist.2) hsne\n rw [hmult, Nat.cast_one] at h3\n have e : s - -2 * (n : \u2102) = s + 2 * (n : \u2102) := by ring\n rw [e] at h3\n linear_combination h3\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 = Wtriv s - seriesFun s + 1 / s + 1 / (s - 1)\n - (Real.log Real.pi : \u2102) / 2 + Hsub n (s / 2) / 2\n rw [hlog, hdig]\n 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, one_div_div]\n ring\n linear_combination h1\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 610,
"oldLines": 7,
"newStart": 610,
"newLines": 9,
"lines": [
" ((differentiableAt_id.add (differentiableAt_const _)).add (differentiableAt_const _))",
" hwj",
" exact (differentiableAt_const _).sub h2",
"- exact hdiff.analyticOnNhd Metric.isOpen_ball",
"+ have hdiff2 : DifferentiableOn \u2102 (digammaSeriesPartSub n)",
"+ (Metric.ball (-(n : \u2102)) (1 / 2)) := hdiff",
"+ exact hdiff2.analyticOnNhd Metric.isOpen_ball",
" ",
" /-- The single-term split: for w \u2208 ball(\u2212n, 1/2), w \u2260 \u2212n,",
" digammaSeriesPart w = digammaSeriesPartSub n w + (1/n \u2212 1/(w+n)). -/"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"The links in the card sections use `--accent` (#4f9cf9) on dark card background? Actually .tbl a uses accent color; but links inside .card outside tables — there's no general `a` styling, so default browser link color (dark blue) shows, hard to read on dark background. Fix: add global link styling for content area links.\n\nAdd to CSS:\n```css\n#content a { color: #7fb8ff; }\n#content a:hover { color: #a8ccff; }\n```\nBut careful not to override menu (menu has its own rules — menu is in #sidebar, so #content a won't affect it). .navbtn and .msg-open have own colors — more specific selectors win over #content a? .navbtn is class selector (0,1,0) vs #content a (1,0,1) — ID selector wins! #content a would override .navbtn color. To be safe, define:\n```css\n#content a { color: #7fb8ff; }\n#content a:hover { color: #b3d4ff; }\n```\nand re-specify exceptions: .navbtn (already has color, need higher specificity: #content .navbtn or add !important... simpler: use `:where()` to keep specificity low: `#content a:where(:not(.navbtn):not(.msg-open))`. :where has zero specificity, so `a:where(...)` total specificity = (0,0,1) + element... `#content` counts though. Let me do: `#content a:not(.navbtn):not(.msg-open)` — specificity (1,2,1) vs .navbtn (0,1,0) → still wins for .navbtn? :not() adds the inner selector's specificity: (1 id, 2 classes, 1 element) > (0,1,0). So it would still override .navbtn. Hmm.\n\nCleanest: only style links that don't have a class:\n```css\n#content a:not([class]) { color: #8fbfff; }\n#content a:not([class]):hover { color: #c0d9ff; text-decoration: underline; }\n```\nSpecificity doesn't matter since others have classes. All plain content links (ledger links? those are in .tbl a — classless! .tbl a currently accent #4f9cf9. The #content a:not([class]) (1,1,1... actually :not([class]) is attribute selector = class-level: (1 id, 1 attr-class-level, 1 element) beats .tbl a (0,1,1). It would change table link color too — from #4f9cf9 to lighter #8fbfff. Is that OK? Table links were readable enough but slightly brighter is fine/better. Consistency good.\n\nBut .msg-open has class — keeps accent. .navbtn class — keeps. Topbar no links. Good.\n\nApply edit, restart server (CSS static file — served directly, no restart needed for static? Django runserver serves static via staticfiles finder each request — template changes need no restart either actually! Templates are loaded per-request in DEBUG (cached but invalidated). CSS/JS changes: static files served from disk each request. So NO restart needed for template/static changes. Only Python changes need restart. Just edit CSS and verify with curl.","signature":""},{"type":"text","text":"The card-body links fall back to the browser default dark blue — only table links were styled. Adding a global content-link style (class-less links only, so buttons/nav keep their styling)."},{"type":"tool_use","id":"Edit_160","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\web\\dashboard\\static\\dashboard\\style.css","old_string":"h1 { font-size: 26px; margin: 10px 0 14px; }","new_string":"/* content links (class-less anchors in cards/body text) */\n#content a:not([class]) { color: #8fbfff; text-decoration: none; }\n#content a:not([class]):hover { color: #c4dcff; text-decoration: underline; }\n\nh1 { font-size: 26px; margin: 10px 0 14px; }"},"extra_content":null}]