[{"type":"thinking","thinking":"`logDeriv_mul (f := ...) (g := ...) _ hne1 hne2 h1 h2` — signature: logDeriv_mul (x?) (hf0 : f x ≠ 0) (hg0 : g x ≠ 0) (hdf : DifferentiableAt f x) (hdg : DifferentiableAt g x). The first `_` is probably the point x implicit or an explicit arg... `logDeriv_mul _ hne1 hne2 h1 h2` — with f,g pinned, then `_`, then the two nonzeros, then two differentiabilities. The `_` might be the `x` explicit. OK — I'll mirror this call shape exactly: `logDeriv_mul (f := ...) (g := ...) _ hne_f hne_g hdf hdg`.\n\nNow write LiMoments.lean §0–§3. I'll be careful about:\n- namespace/open: mirror LiSqueeze: `open Zeta23 Complex Filter Topology`, `noncomputable section`, `namespace NguyenRH1`.\n- The file end: `end NguyenRH1` then... session-028 gotcha: \"file ends `end NguyenRH1` then `end`\" — that was for a file with two namespaces. LiSqueeze ends with just `end NguyenRH1`? Let me not worry — single namespace: end NguyenRH1.\n\nFor the good-set at 1 within 𝓝[≠]: I need ζ s ≠ 0 from zetaA. Also for gFun at 1 continuity.\n\nAlso `differentiableAt_riemannZeta (hs' : s ≠ 1)` ✓.\n\nxiL differentiability — write with function-level Differentiable combinators:\n```lean\nlemma differentiable_xiL : Differentiable ℂ xiL := by\n  have h1 : Differentiable ℂ (fun s : ℂ => s * (s - 1) / 2) :=\n    (differentiable_id.mul (differentiable_id.sub_const 1)).div_const 2\n  have h2 : Differentiable ℂ (fun s : ℂ => (s - 1) / 2) :=\n    (differentiable_id.sub_const 1).div_const 2\n  have h3 : Differentiable ℂ (fun s : ℂ => s / 2) := differentiable_id.div_const 2\n  exact (h1.mul differentiable_completedZeta₀).sub h2 |>.add h3\n```\nHmm — xiL s := (s*(s−1)/2)·Λ₀(s) − (s−1)/2 + s/2: as functions: (fun s => (s*(s−1)/2)*Λ₀ s) − (fun s => (s−1)/2) + (fun s => s/2) — the combinators produce Differentiable ℂ of the lambda; the def xiL must unfold to match — since xiL is a def, `Differentiable ℂ xiL` — the exact lambda after unfolding: `show Differentiable ℂ (fun s => ...)`? def xiL (s : ℂ) : ℂ := ... so xiL = fun s => ... definitionally; the combinators' lambda is syntactically fun s => (s*(s−1)/2)*Λ₀ s − (s−1)/2 + s/2 — same term shape? `exact` will unify up to defeq — should work since it's the same expression tree modulo beta. If not: `unfold xiL; exact ...`.\n\n- analyticAt_xiL : ∀ s, AnalyticAt ℂ xiL s:\n```lean\nlemma analyticAt_xiL (s : ℂ) : AnalyticAt ℂ xiL s :=\n  (differentiable_xiL.differentiableOn.analyticOnNhd isOpen_univ) s (Set.mem_univ s)\n```\nCheck: DifferentiableOn.analyticOnNhd (h : DifferentiableOn ℂ f s) (hs : IsOpen s) : AnalyticOnNhd ℂ f s ✓ (used in LiSeries). AnalyticOnNhd f univ s (mem) : AnalyticAt f s ✓ def of AnalyticOnNhd.\n\n- xiL_eq_mul: careful with completedRiemannZeta_eq: Λ s = Λ₀ s − 1/s − 1/(1−s). Goal: xiL s = (s*(s−1)/2)*Λ s. rw [xiL, completedRiemannZeta_eq]: goal: (s*(s−1)/2)*(Λ₀ s − 1/s − 1/(1−s)) − (s−1)/2 + s/2 = (s*(s−1)/2)*(Λ₀ s − 1/s − 1/(1−s)). field_simp; ring. Hmm field_simp on goal with divisions: should normalize both sides. Let me instead prove: (s*(s−1)/2)*(Λ₀ s − 1/s − 1/(1−s)) = (s*(s−1)/2)*Λ₀ s − (s−1)/2 + s/2 by field_simp + ring, then the xiL eq follows. Write:\n```lean\nlemma xiL_eq_mul {s : ℂ} (h0 : s ≠ 0) (h1 : s ≠ 1) :\n    xiL s = (s * (s - 1) / 2) * completedRiemannZeta s := by\n  rw [xiL, completedRiemannZeta_eq]\n  have hs1 : s - 1 ≠ 0 := sub_ne_zero.mpr h1\n  field_simp\n  ring\n```\nfield_simp needs the denominators: s, 1−s, and 2 (nonzero literals fine). 1−s ≠ 0: neg_sub... sub_ne_zero.mpr (Ne.symm h1)? 1−s ≠ 0 ⟺ 1 ≠ s. Provide h1s : (1:ℂ) − s ≠ 0 := sub_ne_zero.mpr (Ne.symm h1). OK.\n\n- xiL_zero: `by rw [xiL]; simp` — terms: (0*(0−1)/2)*Λ₀ 0 − (0−1)/2 + 0/2: simp should evaluate 0*x = 0, −(0−1)/2 = 1/2: `by simp [xiL]` maybe; fallback norm_num [xiL]. There might be an issue: completedRiemannZeta₀ 0 remains as an atom multiplied by 0 ✓ simp handles zero_mul. \n\n- xiL_one: similar: (1*0/2)*Λ₀ 1 − 0/2 + 1/2 = 1/2 ✓ simp [xiL].\n\n- xiL_one_sub: \n```lean\nlemma xiL_one_sub (s : ℂ) : xiL (1 - s) = xiL s := by\n  by_cases h0 : s = 0\n  · subst h0\n    show xiL (1 - 0) = xiL 0\n    rw [sub_zero, xiL_one, xiL_zero]\n  by_cases h1 : s = 1\n  · subst h1\n    show xiL (1 - 1) = xiL 1\n    rw [sub_self, xiL_zero, xiL_one]\n  · have h10 : (1:ℂ) - s ≠ 0 := sub_ne_zero.mpr (Ne.symm h0)\n    have h11 : (1:ℂ) - s ≠ 1 := by\n      intro h; apply h0; have := congrArg (fun t => (1:ℂ) - t) h; simpa using this\n    rw [xiL_eq_mul h10 h11, xiL_eq_mul h0 h1, completedRiemannZeta_one_sub]\n    congr 1\n    ring\n```\nCheck: xiL (1−s) = ((1−s)((1−s)−1)/2)·Λ(1−s) = ((1−s)(−s)/2)·Λ(s); xiL s = (s(s−1)/2)Λ(s). congr 1 reduces to (1−s)(1−s−1)/2 = s(s−1)/2 ✓ ring. Hmm — (1−s)−1 vs −s: ring handles.\n\n- xiL_ne_zero:\n```lean\nlemma xiL_ne_zero {s : ℂ} (h0 : s ≠ 0) (h1 : s ≠ 1) (hζ : riemannZeta s ≠ 0) : xiL s ≠ 0 := by\n  rw [xiL_eq_mul h0 h1]\n  apply mul_ne_zero\n  · -- s(s−1)/2 ≠ 0\n    have hs1 : s - 1 ≠ 0 := sub_ne_zero.mpr h1\n    exact div_ne_zero (mul_ne_zero h0 hs1) two_ne_zero\n  · -- Λ s ≠ 0\n    intro hΛ\n    rw [completedRiemannZeta_eq_zero_iff] at hΛ\n    exact hζ hΛ.1\n```\ncompletedRiemannZeta_eq_zero_iff's namespace: check — it's in Zeta23/RvM/CountByIntegral.lean; namespace there? The grep showed `lemma completedRiemannZeta_eq_zero_iff {s : ℂ} :` at :65 — need the namespace context. LiFEntire used it — grep LiFEntire for how it's referenced (Zeta23. prefix or open). I'll check quickly.\n\n- not_isNontrivialZero_zero/one ✓ as planned.\n\n- isNontrivialZero_one_sub:\n```lean\nlemma isNontrivialZero_one_sub {ρ : ℂ} (hρ : IsNontrivialZero ρ) :\n    IsNontrivialZero (1 - ρ) := by\n  have h := Zeta23.zeta_reflect_zero ρ (isNontrivialZero_conj hρ)\n  -- reflect (conj ρ) = 1 − conj(conj ρ) = 1 − ρ\n  have e : Zeta23.reflect ((starRingEnd ℂ) ρ) = 1 - ρ := by\n    rw [Zeta23.reflect]  -- unfold def: 1 − starRingEnd (starRingEnd ρ)\n    simp\n  rwa [e] at h\n```\nzeta_reflect_zero namespace: it's in Zeta23/ZetaReflect.lean — namespace Zeta23? presumably `theorem zeta_reflect_zero` inside namespace Zeta23 ✓ (the grep showed `theorem zeta_reflect_zero` — with `open Zeta23` plain `zeta_reflect_zero` works). reflect def: Zeta23.Defs.lean:108 `def reflect (ρ : ℂ) : ℂ := 1 - (starRingEnd ℂ) ρ` — namespace Zeta23 presumably; with open Zeta23, `reflect` might conflict with... let me qualify Zeta23.reflect.\ne: reflect (conj ρ) = 1 − starRingEnd (starRingEnd ℂ ρ) = 1 − ρ: rw [Zeta23.reflect] unfolds (if it's a plain def, rw works with the equation lemma reflect.eq... or `show (1 : ℂ) - (starRingEnd ℂ) ((starRingEnd ℂ) ρ) = 1 - ρ`; simp [starRingEnd_apply]... starRingEnd (starRingEnd x) = x: simp lemma `starRingEnd_self_apply`?? I believe `starRingEnd_self_apply : starRingEnd R (starRingEnd R x) = x` hmm or via `RingHom... ` — simp [Zeta23.reflect] might fully reduce. Fallback: rw [Zeta23.reflect]; congr 1; exact starRingEnd_self_apply... I'll write simp [Zeta23.reflect] and adjust.\n\n- conjZeroEquiv/oneSubZeroEquiv ✓ as planned with `by simp` for involutivity (conj conj; 1−(1−ρ)): for oneSub: Subtype.ext (by simp : (1:ℂ) − (1 − ρ.1) = ρ.1): simp [sub_sub_cancel]... `sub_sub_cancel : a − (a − b) = b` ✓ simp lemma. For conj: starRingEnd involutive ✓.\n\n- good_half_ne_neg_nat ✓.\n\n- momentB + spec:\n```lean\nnoncomputable def momentB (hZC : ZeroCountProp) : ℂ := Classical.choose (partialFraction_identity hZC)\nlemma momentB_spec (hZC : ZeroCountProp) (s : ℂ) (hζ : riemannZeta s ≠ 0) (h0 : s ≠ 0) (h1 : s ≠ 1)\n    (hn : ∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) :\n    logDeriv riemannZeta s = momentB hZC + seriesFun s - 1 / s - 1 / (s - 1) +\n      (Real.log Real.pi : ℂ) / 2 - Complex.digamma (s / 2) / 2 :=\n  Classical.choose_spec (partialFraction_identity hZC) s hζ h0 h1 hn\n```\n\n- gFun:\n```lean\nnoncomputable def gFun (s : ℂ) : ℂ := logDeriv xiL s\n```\n\n- gFun_eq_momentB (hZC) at good s — the §2 chain. Let me be careful about the eventuallyEq Λ = ΓR·ζ:\n```lean\nhave hΓ0 : Complex.Gammaℝ s ≠ 0 := by\n  rw [Ne, Complex.Gammaℝ_eq_zero_iff]\n  push_neg\n  intro m\n  rcases Nat.eq_zero_or_pos m with hm | hm\n  · subst hm; simp; exact h0  -- s ≠ −2·0 = 0\n  · exact hn m hm\n```\nGammaℝ_eq_zero_iff exact form — check: `Complex.Gammaℝ_eq_zero_iff {s : ℂ} : Complex.Gammaℝ s = 0 ↔ ∃ m : ℕ, s = -2 * (m : ℂ)`? From session-029 note \"Gammaℝ_eq_zero_iff gives −(2*↑m)\" — the existential witness form s = −2·↑m with the cast pattern −(2*↑m)? Need to check the exact literal form to match hn's `-2 * (n:ℂ)`. Grep Mathlib when writing. If forms mismatch (e.g. -(2*(m:ℂ)) vs -2*(m:ℂ)), small conversions.\n\nAlso hΓ near s: `(differentiableAt_Gammaℝ_of_not_neg_nat hhalf).continuousAt.eventually_ne hΓ0` : ∀ᶠ t in 𝓝 s, Gammaℝ t ≠ 0 ✓.\n\neventuallyEq Λ = ΓR·ζ:\n```lean\nhave hΛeq : ∀ᶠ t in 𝓝 s, completedRiemannZeta t = Complex.Gammaℝ t * riemannZeta t := by\n  filter_upwards [(differentiableAt_Gammaℝ_of_not_neg_nat hhalf).continuousAt.eventually_ne hΓ0,\n    eventually_ne_nhds h0] with t ht t0\n  -- ζ t = Λ t / ΓR t (riemannZeta_def_of_ne_zero t0); Λ t = ΓR t · ζ t\n  rw [riemannZeta_def_of_ne_zero t0]\n  field_simp [ht]\n```\nriemannZeta_def_of_ne_zero ht : riemannZeta t = completedRiemannZeta t / Gammaℝ t. Goal: Λ t = ΓR t · (Λ t / ΓR t) = Λ t ✓: rw then field_simp [ht] or exact (mul_div_cancel₀ ...).symm: (mul_div_cancel_left₀? `mul_div_cancel_left₀ (h : b ≠ 0) : b * (a / b) = a`? hmm — mul_div_cancel_left₀ : a * (b / a) = b? — `mul_div_cancel_left₀ (ha : a ≠ 0) : a * (b / a) = b`? I think `mul_div_cancel_left₀` exists with that shape... use field_simp robustly.)\n\nThen:\n```lean\ntheorem gFun_eq_momentB (hZC : ZeroCountProp) {s : ℂ} (hζ : riemannZeta s ≠ 0)\n    (h0 : s ≠ 0) (h1 : s ≠ 1) (hn : ∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) :\n    gFun s = momentB hZC + seriesFun s := by\n  have hhalf : ∀ m : ℕ, s / 2 ≠ -(m : ℂ) := good_half_ne_neg_nat h0 hn\n  -- eventuallyEq xiL = product form\n  have hopen : IsOpen ({0}ᶜ ∩ {1}ᶜ : Set ℂ) := isOpen_compl_singleton.inter isOpen_compl_singleton\n  have hexp : ∀ᶠ t in 𝓝 s, xiL t = (t * (t - 1) / 2) * completedRiemannZeta t := by\n    filter_upwards [hopen.mem_nhds ⟨h0, h1⟩] with t ht\n    exact xiL_eq_mul ht.1 ht.2\n  have hlog : logDeriv xiL s = logDeriv (fun t => (t * (t - 1) / 2) * completedRiemannZeta t) s := by\n    have h1' : deriv xiL s = deriv (fun t => (t * (t - 1) / 2) * completedRiemannZeta t) s := hexp.deriv_eq\n    have h2' : xiL s = (s * (s - 1) / 2) * completedRiemannZeta s := hexp.eq_of_nhds\n    rw [gFun, logDeriv, logDeriv, h1', h2']  -- hmm logDeriv is a def: `logDeriv f x = deriv f x / f x`; rw [logDeriv] may not unfold — use `show` or `simp only [logDeriv]`\n  ...\n```\nHmm — logDeriv: `def logDeriv (f : 𝕜 → 𝕜) (x : 𝕜) := deriv f x / f x`? In Mathlib: `logDeriv f x := deriv f x / f x` — there's `logDeriv_apply : logDeriv f x = deriv f x / f x`?? The LiCircleBound usage: `rw [logDeriv_apply]` at :2929 — so `logDeriv_apply` is the unfolding equation ✓ use that: rw [gFun, logDeriv_apply, logDeriv_apply, h1', h2'].\n\nContinue:\n```lean\n  rw [gFun, hlog]\n  have hP : DifferentiableAt ℂ (fun t : ℂ => t * (t - 1) / 2) s :=\n    ((differentiableAt_id.mul (differentiableAt_id.sub_const 1)).div_const 2)\n  have hΛ : DifferentiableAt ℂ completedRiemannZeta s := differentiableAt_completedZeta h0 h1\n  have hP0 : s * (s - 1) / 2 ≠ 0 := div_ne_zero (mul_ne_zero h0 (sub_ne_zero.mpr h1)) two_ne_zero\n  have hΛ0 : completedRiemannZeta s ≠ 0 := by\n    rw [Ne, completedRiemannZeta_eq_zero_iff]; rintro h; exact hζ h.1\n  rw [logDeriv_mul (f := fun t : ℂ => t * (t - 1) / 2) (g := completedRiemannZeta) _ hP0 hΛ0 hP hΛ]\n  -- logDeriv P = 1/s + 1/(s−1)\n  have hPlog : logDeriv (fun t : ℂ => t * (t - 1) / 2) s = 1 / s + 1 / (s - 1) := by\n    rw [logDeriv_apply]\n    have hderiv : deriv (fun t : ℂ => t * (t - 1) / 2) s = s - 1 / 2 := by\n      have hh : HasDerivAt (fun t : ℂ => t * (t - 1) / 2) (s - 1 / 2) s := by\n        have h1' := (hasDerivAt_id' s).mul ((hasDerivAt_id' s).sub_const 1)\n        -- (t·(t−1))' = (t−1) + t = 2t−1... then /2\n        have h2' := h1'.div_const 2\n        convert h2' using 1\n        ring\n      exact hh.deriv\n    rw [hderiv]\n    have hs1 : s - 1 ≠ 0 := sub_ne_zero.mpr h1\n    field_simp\n    ring\n  rw [hPlog]\n  -- logDeriv Λ = logDeriv ΓR + logDeriv ζ\n  have hlogΛ : logDeriv completedRiemannZeta s = logDeriv Complex.Gammaℝ s + logDeriv riemannZeta s := by\n    have heq : logDeriv completedRiemannZeta s =\n        logDeriv (fun t => Complex.Gammaℝ t * riemannZeta t) s := by\n      rw [logDeriv_apply, logDeriv_apply, hΛeq.deriv_eq, hΛeq.eq_of_nhds]\n    rw [heq, logDeriv_mul (f := Complex.Gammaℝ) (g := riemannZeta) _ hΓ0 hζ\n      (differentiableAt_Gammaℝ_of_not_neg_nat hhalf) (differentiableAt_riemannZeta h1)]\n  rw [hlogΛ, logDeriv_Gammaℝ_eq_of_not_neg_nat hhalf, momentB_spec hZC s hζ h0 h1 hn]\n  ring\n```\nWait — HasDerivAt for t·(t−1): (hasDerivAt_id' s).mul (hasDerivAt (t−1)): HasDerivAt.mul : HasDerivAt f a x → HasDerivAt g b x → HasDerivAt (f·g) (a·g x + f x·b) x: with f = id (a = 1), g = t−1 (b = 1): derivative = 1·(s−1) + s·1 = 2s−1. Then div_const 2: (2s−1)/2 = s − 1/2: the convert+ring aligns the derivative value forms. Careful: HasDerivAt.mul's value form might be `1 * (s - 1) + s * 1` — convert via ring ✓. hasDerivAt_id' : HasDerivAt id 1 s? `hasDerivAt_id' (x) : HasDerivAt id 1 x`? hmm — (hasDerivAt_id' s).sub_const 1 : HasDerivAt (fun t => t − 1) (1 − 0) s ✓. The `.mul` — signature HasDerivAt.mul (ha : HasDerivAt f f' x) (hb : HasDerivAt g g' x) : HasDerivAt (fun x => f x * g x) (f' * g x + f x * g') x? (the product rule form). Then div_const: (f'*g + f*g')/2. convert+ring handles.\n\nAlso note: deriv of P written as fun t => t*(t−1)/2 — parses as (t*(t−1))/2 ✓.\n\n- §3 bridges:\n```lean\nlemma eq_of_eventuallyEq_nhd_ne {F G : ℂ → ℂ} {s₀ : ℂ} (hF : ContinuousAt F s₀)\n    (hG : ContinuousAt G s₀) (h : F =ᶠ[𝓝[≠] s₀] G) : F s₀ = G s₀ :=\n  tendsto_nhds_unique (hF.tendsto.mono_left nhdsWithin_le_nhds)\n    ((hG.tendsto.mono_left nhdsWithin_le_nhds).congr' h.symm)\n```\nCheck: Tendsto.congr' : f₁ =ᶠ[l] f₂ → Tendsto f₁ l L → Tendsto f₂ l L. hG' : Tendsto G (𝓝[≠] s₀) (𝓝 (G s₀)); h.symm : G =ᶠ[𝓝[≠]] F; hG'.congr' h.symm : Tendsto F (𝓝[≠]) (𝓝 (G s₀)) ✓. tendsto_nhds_unique : [NeBot l] → Tendsto f l (𝓝 a) → Tendsto f l (𝓝 b) → a = b ✓ (NeBot (𝓝[≠] s₀) instance ✓).\n\n- gFun continuousAt:\n```lean\nlemma gFun_continuousAt (s : ℂ) (hs : xiL s ≠ 0) : ContinuousAt gFun s :=\n  (((analyticAt_xiL s).deriv).div (analyticAt_xiL s) hs).continuousAt\n```\ngFun = logDeriv xiL = fun s => deriv xiL s / xiL s — the AnalyticAt.div produces AnalyticAt (deriv xiL / xiL) s — needs gFun s =ᶠ or defeq: gFun s := logDeriv xiL s = deriv xiL s / xiL s — the function logDeriv xiL vs (deriv xiL / xiL): Pi.div: (f/g) x = f x / g x ✓ defeq with logDeriv_apply. AnalyticAt.div : AnalyticAt f → AnalyticAt g → g x ≠ 0 → AnalyticAt (f / g) — target function (deriv xiL / xiL) = logDeriv xiL: defeq but the statement needs show: `show ContinuousAt (fun s => deriv xiL s / xiL s) s`? gFun s — ContinuousAt gFun s — unfold: `by show ContinuousAt (fun s => deriv xiL s / xiL s) s; exact ...`? gFun is a def: ContinuousAt gFun s where gFun = fun s => logDeriv xiL s = fun s => deriv xiL s / xiL s: the div on functions: deriv xiL s / xiL s = (deriv xiL / xiL) s by Pi.div_apply ✓ defeq. `exact` should unify. I'll write it with a show bridge if needed.\n\n- seriesFun continuousAt: (seriesFun_analyticAt hs₀).continuousAt ✓.\n\n- good-eventually at 0 and 1:\n```lean\nlemma good_eventually_zero : ∀ᶠ s in 𝓝[≠] (0:ℂ), riemannZeta s ≠ 0 ∧ s ≠ 1 ∧\n    (∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) := by\n  have hζ : ∀ᶠ s in 𝓝 (0:ℂ), riemannZeta s ≠ 0 :=\n    (analyticAt_riemannZeta (by norm_num : (0:ℂ) ≠ 1)).continuousAt.eventually_ne\n      (by rw [riemannZeta_zero]; norm_num)\n  have h1 : ∀ᶠ s in 𝓝 (0:ℂ), s ≠ 1 := eventually_ne_nhds (by norm_num : (0:ℂ) ≠ 1)\n  have hnorm : ∀ᶠ s in 𝓝 (0:ℂ), ‖s‖ < 2 := by\n    have h : Metric.ball (0:ℂ) 2 ∈ 𝓝 (0:ℂ) := Metric.ball_mem_nhds _ (by norm_num)\n    filter_upwards [h] with s hs\n    rw [Metric.mem_ball, dist_zero_right] at hs\n    exact hs\n  filter_upwards [hζ.filter_mono nhdsWithin_le_nhds, h1.filter_mono nhdsWithin_le_nhds,\n    hnorm.filter_mono nhdsWithin_le_nhds] with s hζs h1s hsn\n  refine ⟨hζs, h1s, fun n hn1 => ?_⟩\n  intro h\n  rw [h] at hsn\n  have : (2:ℝ) ≤ ‖(-2 : ℂ) * (n : ℂ)‖ := by\n    rw [norm_mul, norm_neg, norm_two??]  -- ‖(−2:ℂ)‖ = 2; ‖(n:ℂ)‖ = n ≥ 1\n    ...\n  linarith [this, hsn]  -- 2 ≤ ‖s‖ < 2 contradiction\n```\nnorm computations: ‖(−2:ℂ)‖ = 2: `norm_neg` then norm of (2:ℂ): `Complex.norm_two`? hmm — norm_num can: ‖(-2:ℂ)‖ via `by norm_num`? For casts: ‖((−2:ℕ...)): careful the term is -2 * (n:ℂ) — norm_mul: ‖−2‖·‖(n:ℂ)‖ = 2·n (n ≥ 1): ≥ 2. norm_num [norm_mul, Complex.norm_natCast]? There's `Complex.norm_natCast : ‖(n:ℂ)‖ = n` ✓ and ‖(−2:ℂ)‖: rw [norm_neg]; norm_num? `Complex.norm_ofNat`? I'll do: have : ‖(-2 : ℂ)‖ = 2 := by norm_num [norm_neg]... robust: (show ‖(-2:ℂ)‖ = 2 by rw [norm_neg]; exact norm_ofNat...). Simpler: push through: ‖(−2:ℂ)‖ = ‖((2:ℝ):ℂ)‖ = 2 by norm_num1? I'll write `by norm_num [norm_neg, Complex.norm_natCast]` and fix at build. Then n ≥ 1: (1:ℝ) ≤ n: Nat.one_le_cast.mpr hn1. So 2·n ≥ 2 ✓ linarith.\n\n- good_eventually_one: at 1: hζ via zetaA:\n```lean\nlemma good_eventually_one : ∀ᶠ s in 𝓝[≠] (1:ℂ), riemannZeta s ≠ 0 ∧ s ≠ 0 ∧\n    (∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) := by\n  have hA : ∀ᶠ s in 𝓝 (1:ℂ), zetaA s ≠ 0 := zetaA_ne_zero_near_one\n  have h0 : ∀ᶠ s in 𝓝 (1:ℂ), s ≠ 0 := eventually_ne_nhds (by norm_num : (1:ℂ) ≠ 0)\n  have hnorm : ∀ᶠ s in 𝓝 (1:ℂ), ‖s‖ < 2 := ... ball_mem_nhds 1 (2) — ball centered 1 radius 2: ‖s−1‖ < 2... hmm I want ‖s‖ < 2? s near 1: ‖s‖ ≤ ‖s−1‖+1 < 3... use radius 1: ‖s−1‖ < 1 ⟹ if s = −2n: ‖−2n − 1‖ ≥ |2n − 1| ≥ 1: for n ≥ 1: |−2n−1| = 2n+1 ≥ 3 > 1 ✓. So radius 1: s = −2n ⟹ ‖s − 1‖ = ‖−2n − 1‖ = 2n+1 ≥ 3 ✗.\n  filter_upwards [hA.filter_mono nhdsWithin_le_nhds, self_mem_nhdsWithin,\n    h0.filter_mono nhdsWithin_le_nhds, hnorm...] with s hAs hs1 h0s hsn\n  -- ζ s ≠ 0: if ζ s = 0 then zetaA s = (s−1)·ζ s = 0 (zetaA_apply hs1) contradiction\n  refine ⟨?_, h0s, fun n hn1 => ?_⟩\n  · intro hζ\n    rw [zetaA_apply hs1, hζ, mul_zero] at hAs\n    exact hAs rfl\n  · intro h; rw [h] at hsn; -- ‖−2n − 1‖ < 1 contradiction\n    ...\n```\nself_mem_nhdsWithin : s ∈ 𝓝[≠] s₀ → s ≠ s₀ ✓ (self_mem_nhdsWithin : {x}ᶜ ∈... : ∀ᶠ y in 𝓝[≠] x, y ≠ x ✓).\n\nWait hnorm at 1: Metric.ball (1:ℂ) 1 ∈ 𝓝 1 ✓; s ∈ ball ⟹ ‖s − 1‖ < 1 (Metric.mem_ball, dist_eq_norm: dist s 1 = ‖s − 1‖ ✓). s = −2·n: ‖(−2n) − 1‖ = ‖−(2n+1)‖ = 2n+1 ≥ 3: compute: (−2:ℂ)·(n:ℂ) − 1 = −(2·n+1): norm = 2n+1 (norm_neg; norm of (2n+1 : ℂ)... via push_cast to real: ‖(−(2*(n:ℝ)+1):ℂ)‖ = |−(2n+1)| = 2n+1). Then 3 ≤ 2n+1 < 1 ✗ linarith. The cast juggling: ‖(-2:ℂ)*(n:ℂ) − 1‖: show = 2*n+1: have e : (-2:ℂ)*(n:ℂ) − 1 = ((−(2*n+1):ℝ):ℂ) := by push_cast; ring; rw [e, Complex.norm_real, Real.norm_eq_abs, abs_neg, abs_of_nonneg (by positivity...)] — n:ℝ ≥ 0: 2n+1 > 0 ✓.\n\n- gFun_zero (hZC):\n```lean\nlemma gFun_zero (hZC : ZeroCountProp) : gFun 0 = momentB hZC := by\n  have hgood : ∀ᶠ s in 𝓝[≠] (0:ℂ), gFun s = momentB hZC + seriesFun s := by\n    filter_upwards [good_eventually_zero, self_mem_nhdsWithin] with s ⟨hζ, h1, hn⟩ h0\n    exact gFun_eq_momentB hZC hζ h0 h1 hn\n  have hF : ContinuousAt gFun 0 := gFun_continuousAt 0 (by rw [xiL_zero]; norm_num)\n  have hG : ContinuousAt (fun s => momentB hZC + seriesFun s) 0 :=\n    continuousAt_const.add (seriesFun_analyticAt not_isNontrivialZero_zero).continuousAt\n  have := eq_of_eventuallyEq_nhd_ne hF hG hgood\n  -- this : gFun 0 = momentB hZC + seriesFun 0; seriesFun 0 = 0\n  rwa [seriesFun_zero, add_zero] at this\n```\n\n- gFun_one (hZC): gFun 1 = momentB hZC + seriesFun 1 — same shape with good_eventually_one, self (s ≠ 1), xiL_one.\n\n- gFun_one_eq_neg: as planned.\n\n- seriesFun_zero, seriesFun_one as planned.\n\nThat's §1–§3 (~400 lines). Write it now. Note: file header comment + imports:\n\nimport Mathlib\nimport NguyenRH1.LiTightR\nimport NguyenRH1.LiSwaps\nimport NguyenRH1.LiResidue\nimport NguyenRH1.LiDigamma\nimport NguyenRH1.LiReflect\n\nWait — LiTightR imports LiSqueeze which imports LiCircleBound which imports LiFEntire (→ LiSeries presumably), LiGapCircles, LiDisc. Does anything import LiReflect in that chain? LiTightR needs sum_nearZeros_neg_reflect? Actually maybe not. Import LiReflect explicitly ✓. LiSwaps (sigmaP) — is it in LiTightR's chain? LiSqueeze→LiCircleBound→LiFEntire→LiSeries→? LiSeries imports (from the head): Mathlib, Zeta23.Statement, Zeta23.FromPNTPlus.ZetaBounds — no LiSwaps. So import LiSwaps ✓. LiDigamma for eventuallyEq_iteratedDeriv/iteratedDeriv_congr_of_eventuallyEq ✓ (needed §5/§6). LiResidue for zetaA ✓.\n\nopen: `open Zeta23 Complex Filter Topology` (mirror LiSqueeze) — also need `open Metric`? LiSeries uses Metric.ball qualified — keep qualified. `open scoped`? The big operators fine.\n\nnoncomputable section + namespace NguyenRH1.\n\nLet me now write the file §0–§3. I'll write the whole thing in one go, then iterate on build errors. Given length constraints, write §0–§3 first (~420 lines), build, fix, then continue with §4–§6.\n\nOne more check: `eventually_ne_nhds` exists? `eventually_ne_nhds (h : a ≠ b) : ∀ᶠ x in 𝓝 a, x ≠ b` ✓ exists (used LiResidue:87).\n\n`Complex.norm_two`? For ‖(−2:ℂ)·(n:ℂ)‖: norm_mul → ‖−2‖·‖n‖: ‖((−2):ℂ)‖: I'll compute via: have h2 : ‖(-2 : ℂ)‖ = 2 := by rw [show (-2:ℂ) = ((-2:ℝ):ℂ) by norm_cast... hmm push_cast: ((-2:ℝ):ℂ) = -2 ✓ by push_cast; ring? norm_num should know: `by norm_num [norm_neg]`? Let me just: ‖(-2:ℂ)‖ = ‖(-(2:ℂ))‖ = ‖(2:ℂ)‖ = 2: norm_neg + Complex.norm_ofNat? `Complex.norm_ofNat : ‖(OfNat.ofNat n : ℂ)‖ = OfNat.ofNat n`? hmm norm_num extension handles norms of numerals ✓ `by norm_num` likely closes ‖(-2:ℂ)‖ = 2 directly (norm_num knows Complex.normSq... risky). Robust: rw [← Complex.ofReal_neg, ← Complex.ofReal_two]?? ofReal_two exists? `Complex.ofReal_ofNat`? Use: ((-2:ℂ)) = ((-2:ℝ):ℂ): by norm_cast; then Complex.norm_real, Real.norm_eq_abs, abs_neg, abs_two... I'll write the robust version:\n```lean\nhave h2 : ‖(-2 : ℂ)‖ = 2 := by\n  rw [show (-2 : ℂ) = ((-2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real,\n    Real.norm_eq_abs, abs_neg]\n  norm_num\n```\nAnd ‖(n:ℂ)‖ = (n:ℝ): Complex.norm_natCast? — `Complex.norm_natCast (n : ℕ) : ‖(n : ℂ)‖ = n` ✓ exists (RCLike.norm_natCast general — earlier code used RCLike.norm_natCast ✓). \n\nAlso for good_eventually_zero's last step: this : 2 ≤ ‖(-2:ℂ)*(n:ℂ)‖: rw [norm_mul, h2, RCLike.norm_natCast]: 2·(n:ℝ) with n ≥ 1: ≥ 2 ✓ linarith [Nat.one_le_cast.mpr hn1...]. hn1 : 1 ≤ n (ℕ): (1:ℝ) ≤ (n:ℝ) := Nat.one_le_cast.mpr hn1 ✓.\n\nWrite it.","signature":""},{"type":"text","text":"`logDeriv_mul` call-shape confirmed. Now writing LiMoments.lean §0–§3 (xiL, the gFun = B + seriesFun identity, and the evaluations at 0/1)."},{"type":"tool_use","id":"Write_52","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiMoments.lean","content":"/-\nLiMoments.lean — tier ii′-3b: the contour moments (M) via the 5e\npartial-fraction identity (D-070 route revision; D-066 §3's rectangle\nplan superseded).\n\nTarget (D-066 §2 piece (M)): for all k ≥ 1,\n  sigmaP k = −(iteratedDeriv (k−1) gFun 0)/(k−1)!,\nwhere gFun = logDeriv xiL and xiL = (s(s−1)/2)·completedRiemannZeta is\nthe entire ξ. The whole argument is the identity\n\n  (G)  gFun s = B + seriesFun s\n\nat every good point (ζ s ≠ 0, s ≠ 0, s ≠ 1, s ≠ −2n for n ≥ 1) — pure\nlogDeriv algebra from 5e's `partialFraction_identity` — plus termwise\nseries calculus: k ≥ 2 by iterated derivation of the absolutely\nsummable zero series at 0 (the LiDigamma §7–8 `iteratedDerivWithin_tsum`\npattern), k = 1 by the conj/reflect reindex V = Σ mult·(1/ρ̄ − 1/(1−ρ))\n= −V = 0 (zeroMult_conj + zeroMult_one_sub).\n\n§1: xiL (entire closed form via completedRiemannZeta₀) + basic facts +\n    the two zero-subtype equivs.\n§2: the good-set lemmas + (G) (`gFun_eq_momentB`).\n§3: evaluation at 0 and 1 (punctured-continuity bridges) + the FE sign\n    (`gFun_one_eq_neg`).\n§4: summability budget + the k = 1 rearrangement (`two_mul_sigmaP_one`).\n§5: the per-term derivative machine + termwise iterated derivation at 0\n    (`iteratedDeriv_seriesFun_zero`).\n§6: the capstone `sigmaP_eq_neg_iteratedDeriv_gFun_div`.\n\nPerimeter: `ZeroCountProp` only (inherited from 5e's gap circles).\nArchive references: D-066 §2, D-068 §5, D-070.\n-/\nimport Mathlib\nimport NguyenRH1.LiTightR\nimport NguyenRH1.LiSwaps\nimport NguyenRH1.LiResidue\nimport NguyenRH1.LiDigamma\nimport NguyenRH1.LiReflect\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The entire ξ and the zero-subtype equivs -/\n\n/-- The entire ξ in closed form: (s(s−1)/2)·Λ₀(s) − (s−1)/2 + s/2 with\nΛ₀ = `completedRiemannZeta₀` entire (Mathlib `differentiable_completedZeta₀`).\nEquals (s(s−1)/2)·Λ(s) off {0, 1} (`xiL_eq_mul`); xiL(0) = xiL(1) = 1/2. -/\ndef xiL (s : ℂ) : ℂ :=\n  (s * (s - 1) / 2) * completedRiemannZeta₀ s - (s - 1) / 2 + s / 2\n\nlemma differentiable_xiL : Differentiable ℂ xiL := by\n  have h1 : Differentiable ℂ (fun s : ℂ => s * (s - 1) / 2) :=\n    (differentiable_id.mul (differentiable_id.sub_const 1)).div_const 2\n  have h2 : Differentiable ℂ (fun s : ℂ => (s - 1) / 2) :=\n    (differentiable_id.sub_const 1).div_const 2\n  have h3 : Differentiable ℂ (fun s : ℂ => s / 2) := differentiable_id.div_const 2\n  exact ((h1.mul differentiable_completedZeta₀).sub h2).add h3\n\nlemma analyticAt_xiL (s : ℂ) : AnalyticAt ℂ xiL s :=\n  (differentiable_xiL.differentiableOn.analyticOnNhd isOpen_univ) s (Set.mem_univ s)\n\n/-- The defining equation off {0, 1}: xiL s = (s(s−1)/2)·Λ(s). -/\nlemma xiL_eq_mul {s : ℂ} (h0 : s ≠ 0) (h1 : s ≠ 1) :\n    xiL s = (s * (s - 1) / 2) * completedRiemannZeta s := by\n  rw [xiL, completedRiemannZeta_eq]\n  have h1s : (1 : ℂ) - s ≠ 0 := sub_ne_zero.mpr (Ne.symm h1)\n  field_simp\n  ring\n\nlemma xiL_zero : xiL 0 = 1 / 2 := by simp [xiL]\n\nlemma xiL_one : xiL 1 = 1 / 2 := by simp [xiL]\n\n/-- The functional equation xiL(1−s) = xiL(s), all s. -/\nlemma xiL_one_sub (s : ℂ) : xiL (1 - s) = xiL s := by\n  by_cases h0 : s = 0\n  · subst h0\n    show xiL (1 - 0) = xiL 0\n    rw [sub_zero, xiL_one, xiL_zero]\n  by_cases h1 : s = 1\n  · subst h1\n    show xiL (1 - 1) = xiL 1\n    rw [sub_self, xiL_zero, xiL_one]\n  · have h10 : (1 : ℂ) - s ≠ 0 := sub_ne_zero.mpr (Ne.symm h0)\n    have h11 : (1 : ℂ) - s ≠ 1 := by\n      intro h\n      apply h0\n      have h2 := congrArg (fun t : ℂ => (1 : ℂ) - t) h\n      simp at h2\n      exact h2\n    rw [xiL_eq_mul h10 h11, xiL_eq_mul h0 h1, completedRiemannZeta_one_sub]\n    congr 1\n    ring\n\n/-- xiL vanishes nowhere off {0, 1} where ζ ≠ 0. -/\nlemma xiL_ne_zero {s : ℂ} (h0 : s ≠ 0) (h1 : s ≠ 1) (hζ : riemannZeta s ≠ 0) :\n    xiL s ≠ 0 := by\n  rw [xiL_eq_mul h0 h1]\n  apply mul_ne_zero\n  · exact div_ne_zero (mul_ne_zero h0 (sub_ne_zero.mpr h1)) two_ne_zero\n  · intro hΛ\n    rw [completedRiemannZeta_eq_zero_iff] at hΛ\n    exact hζ hΛ.1\n\nlemma not_isNontrivialZero_zero : ¬ IsNontrivialZero (0 : ℂ) := by\n  intro h\n  have h2 := h.2.1\n  rw [Complex.zero_re] at h2\n  exact lt_irrefl 0 h2\n\nlemma not_isNontrivialZero_one : ¬ IsNontrivialZero (1 : ℂ) := by\n  intro h\n  have h2 := h.2.2\n  rw [Complex.one_re] at h2\n  exact lt_irrefl 1 h2\n\n/-- Reflection of a nontrivial zero: 1 − ρ is a nontrivial zero\n(conj then Zeta23 reflect). -/\nlemma isNontrivialZero_one_sub {ρ : ℂ} (hρ : IsNontrivialZero ρ) :\n    IsNontrivialZero (1 - ρ) := by\n  have h := zeta_reflect_zero ρ (isNontrivialZero_conj hρ)\n  have e : Zeta23.reflect ((starRingEnd ℂ) ρ) = 1 - ρ := by\n    simp [Zeta23.reflect]\n  rwa [e] at h\n\n/-- The conjugation involution on the nontrivial-zero subtype. -/\ndef conjZeroEquiv : {ρ : ℂ // IsNontrivialZero ρ} ≃ {ρ : ℂ // IsNontrivialZero ρ} where\n  toFun ρ := ⟨(starRingEnd ℂ) ρ, isNontrivialZero_conj ρ.2⟩\n  invFun ρ := ⟨(starRingEnd ℂ) ρ, isNontrivialZero_conj ρ.2⟩\n  left_inv ρ := Subtype.ext (by simp)\n  right_inv ρ := Subtype.ext (by simp)\n\n/-- The reflection involution ρ ↦ 1 − ρ on the nontrivial-zero subtype. -/\ndef oneSubZeroEquiv : {ρ : ℂ // IsNontrivialZero ρ} ≃ {ρ : ℂ // IsNontrivialZero ρ} where\n  toFun ρ := ⟨1 - ρ, isNontrivialZero_one_sub ρ.2⟩\n  invFun ρ := ⟨1 - ρ, isNontrivialZero_one_sub ρ.2⟩\n  left_inv ρ := Subtype.ext (by simp)\n  right_inv ρ := Subtype.ext (by simp)\n\n/-! ## 2. The good set and the identity (G) -/\n\n/-- The chosen constant from the 5e partial-fraction identity. -/\nnoncomputable def momentB (hZC : ZeroCountProp) : ℂ :=\n  Classical.choose (partialFraction_identity hZC)\n\nlemma momentB_spec (hZC : ZeroCountProp) (s : ℂ) (hζ : riemannZeta s ≠ 0)\n    (h0 : s ≠ 0) (h1 : s ≠ 1) (hn : ∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) :\n    logDeriv riemannZeta s = momentB hZC + seriesFun s - 1 / s - 1 / (s - 1) +\n      (Real.log Real.pi : ℂ) / 2 - Complex.digamma (s / 2) / 2 :=\n  Classical.choose_spec (partialFraction_identity hZC) s hζ h0 h1 hn\n\n/-- The log-derivative of ξ. -/\nnoncomputable def gFun (s : ℂ) : ℂ := logDeriv xiL s\n\n/-- The good-set half-shift condition for the ΓR identity: s/2 ∉ −ℕ. -/\nlemma good_half_ne_neg_nat {s : ℂ} (h0 : s ≠ 0)\n    (hn : ∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) :\n    ∀ m : ℕ, s / 2 ≠ -(m : ℂ) := by\n  intro m hm\n  rcases Nat.eq_zero_or_pos m with hm0 | hm0\n  · subst hm0\n    simp only [Nat.cast_zero, neg_zero] at hm\n    exact h0 (by linarith [hm])\n  · apply hn m hm0\n    have h2 : s = -2 * (s / 2) := by ring\n    rw [h2, hm]\n    ring\n\n/-- **The identity (G)**: off the excluded set, gFun = B + seriesFun.\nPure logDeriv algebra: logDeriv of xiL = (s(s−1)/2)·Λ splits as\n1/s + 1/(s−1) + [−(log π)/2 + ψ(s/2)/2] + ζ′/ζ, and 5e's\npartial-fraction identity collapses everything to B + seriesFun. -/\ntheorem gFun_eq_momentB (hZC : ZeroCountProp) {s : ℂ} (hζ : riemannZeta s ≠ 0)\n    (h0 : s ≠ 0) (h1 : s ≠ 1) (hn : ∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) :\n    gFun s = momentB hZC + seriesFun s := by\n  have hhalf : ∀ m : ℕ, s / 2 ≠ -(m : ℂ) := good_half_ne_neg_nat h0 hn\n  have hΓ0 : Complex.Gammaℝ s ≠ 0 := by\n    rw [Ne, Complex.Gammaℝ_eq_zero_iff]\n    push_neg\n    intro m\n    rcases Nat.eq_zero_or_pos m with hm | hm\n    · subst hm\n      simp only [Nat.cast_zero, mul_zero, neg_zero]\n      exact h0\n    · exact hn m hm\n  have hΓdiff : DifferentiableAt ℂ Complex.Gammaℝ s :=\n    differentiableAt_Gammaℝ_of_not_neg_nat hhalf\n  -- xiL agrees with the product form on a neighbourhood of s\n  have hopen : IsOpen ({0}ᶜ ∩ {1}ᶜ : Set ℂ) :=\n    isOpen_compl_singleton.inter isOpen_compl_singleton\n  have hexp : ∀ᶠ t in 𝓝 s, xiL t = (t * (t - 1) / 2) * completedRiemannZeta t := by\n    filter_upwards [hopen.mem_nhds ⟨h0, h1⟩] with t ht\n    exact xiL_eq_mul ht.1 ht.2\n  -- Λ agrees with ΓR·ζ on a neighbourhood of s\n  have hΛeq : ∀ᶠ t in 𝓝 s, completedRiemannZeta t = Complex.Gammaℝ t * riemannZeta t := by\n    filter_upwards [hΓdiff.continuousAt.eventually_ne hΓ0, eventually_ne_nhds h0]\n      with t htΓ ht0\n    rw [riemannZeta_def_of_ne_zero ht0]\n    field_simp [htΓ]\n  have hlog : logDeriv xiL s =\n      logDeriv (fun t => (t * (t - 1) / 2) * completedRiemannZeta t) s := by\n    rw [logDeriv_apply, logDeriv_apply, hexp.deriv_eq, hexp.eq_of_nhds]\n  rw [gFun, hlog]\n  have hP : DifferentiableAt ℂ (fun t : ℂ => t * (t - 1) / 2) s :=\n    (differentiableAt_id.mul (differentiableAt_id.sub_const 1)).div_const 2\n  have hΛ : DifferentiableAt ℂ completedRiemannZeta s := differentiableAt_completedZeta h0 h1\n  have hP0 : s * (s - 1) / 2 ≠ 0 :=\n    div_ne_zero (mul_ne_zero h0 (sub_ne_zero.mpr h1)) two_ne_zero\n  have hΛ0 : completedRiemannZeta s ≠ 0 := by\n    rw [Ne, completedRiemannZeta_eq_zero_iff]\n    rintro h\n    exact hζ h.1\n  rw [logDeriv_mul (f := fun t : ℂ => t * (t - 1) / 2) (g := completedRiemannZeta) _\n    hP0 hΛ0 hP hΛ]\n  have hPlog : logDeriv (fun t : ℂ => t * (t - 1) / 2) s = 1 / s + 1 / (s - 1) := by\n    rw [logDeriv_apply]\n    have hderiv : deriv (fun t : ℂ => t * (t - 1) / 2) s = s - 1 / 2 := by\n      have hh : HasDerivAt (fun t : ℂ => t * (t - 1) / 2) (s - 1 / 2) s := by\n        have h1' := (hasDerivAt_id' s).mul ((hasDerivAt_id' s).sub_const 1)\n        have h2' := h1'.div_const 2\n        convert h2' using 1\n        ring\n      exact hh.deriv\n    rw [hderiv]\n    have hs1 : s - 1 ≠ 0 := sub_ne_zero.mpr h1\n    field_simp\n    ring\n  rw [hPlog]\n  have hlogΛ : logDeriv completedRiemannZeta s =\n      logDeriv Complex.Gammaℝ s + logDeriv riemannZeta s := by\n    have heq : logDeriv completedRiemannZeta s =\n        logDeriv (fun t => Complex.Gammaℝ t * riemannZeta t) s := by\n      rw [logDeriv_apply, logDeriv_apply, hΛeq.deriv_eq, hΛeq.eq_of_nhds]\n    rw [heq, logDeriv_mul (f := Complex.Gammaℝ) (g := riemannZeta) _ hΓ0 hζ\n      (differentiableAt_Gammaℝ_of_not_neg_nat hhalf) (differentiableAt_riemannZeta h1)]\n  rw [hlogΛ, logDeriv_Gammaℝ_eq_of_not_neg_nat hhalf, momentB_spec hZC s hζ h0 h1 hn]\n  ring\n\n/-! ## 3. Evaluation at 0 and 1 -/\n\n/-- Functions continuous at s₀ that agree on the punctured neighbourhood\nagree at s₀. -/\nlemma eq_of_eventuallyEq_nhd_ne {F G : ℂ → ℂ} {s₀ : ℂ} (hF : ContinuousAt F s₀)\n    (hG : ContinuousAt G s₀) (h : F =ᶠ[𝓝[≠] s₀] G) : F s₀ = G s₀ :=\n  tendsto_nhds_unique (hF.tendsto.mono_left nhdsWithin_le_nhds)\n    ((hG.tendsto.mono_left nhdsWithin_le_nhds).congr' h.symm)\n\n/-- gFun is continuous wherever xiL ≠ 0. -/\nlemma gFun_continuousAt (s : ℂ) (hs : xiL s ≠ 0) : ContinuousAt gFun s :=\n  (((analyticAt_xiL s).deriv).div (analyticAt_xiL s) hs).continuousAt\n\n/-- The good conditions hold eventually in the punctured neighbourhood of 0. -/\nlemma good_eventually_zero :\n    ∀ᶠ s in 𝓝[≠] (0 : ℂ), riemannZeta s ≠ 0 ∧ s ≠ 1 ∧\n      (∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) := by\n  have hζ : ∀ᶠ s in 𝓝 (0 : ℂ), riemannZeta s ≠ 0 :=\n    (analyticAt_riemannZeta (by norm_num : (0 : ℂ) ≠ 1)).continuousAt.eventually_ne\n      (by rw [riemannZeta_zero]; norm_num)\n  have h1 : ∀ᶠ s in 𝓝 (0 : ℂ), s ≠ 1 := eventually_ne_nhds (by norm_num : (0 : ℂ) ≠ 1)\n  have hnorm : ∀ᶠ s in 𝓝 (0 : ℂ), ‖s‖ < 2 := by\n    have h : Metric.ball (0 : ℂ) 2 ∈ 𝓝 (0 : ℂ) := Metric.ball_mem_nhds _ (by norm_num)\n    filter_upwards [h] with s hs\n    rw [Metric.mem_ball, dist_zero_right] at hs\n    exact hs\n  filter_upwards [hζ.filter_mono nhdsWithin_le_nhds, h1.filter_mono nhdsWithin_le_nhds,\n    hnorm.filter_mono nhdsWithin_le_nhds] with s hζs h1s hsn\n  refine ⟨hζs, h1s, fun n hn1 habs => ?_⟩\n  rw [habs] at hsn\n  have h2 : ‖(-2 : ℂ)‖ = 2 := by\n    rw [show (-2 : ℂ) = ((-2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real,\n      Real.norm_eq_abs, abs_neg]\n    norm_num\n  have hbig : (2 : ℝ) ≤ ‖(-2 : ℂ) * (n : ℂ)‖ := by\n    rw [norm_mul, h2, RCLike.norm_natCast]\n    have hn1' : (1 : ℝ) ≤ (n : ℝ) := Nat.one_le_cast.mpr hn1\n    linarith\n  linarith\n\n/-- The good conditions hold eventually in the punctured neighbourhood of 1. -/\nlemma good_eventually_one :\n    ∀ᶠ s in 𝓝[≠] (1 : ℂ), riemannZeta s ≠ 0 ∧ s ≠ 0 ∧\n      (∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) := by\n  have hA : ∀ᶠ s in 𝓝 (1 : ℂ), zetaA s ≠ 0 := zetaA_ne_zero_near_one\n  have h0 : ∀ᶠ s in 𝓝 (1 : ℂ), s ≠ 0 := eventually_ne_nhds (by norm_num : (1 : ℂ) ≠ 0)\n  have hnorm : ∀ᶠ s in 𝓝 (1 : ℂ), ‖s - 1‖ < 1 := by\n    have h : Metric.ball (1 : ℂ) 1 ∈ 𝓝 (1 : ℂ) := Metric.ball_mem_nhds _ (by norm_num)\n    filter_upwards [h] with s hs\n    rw [Metric.mem_ball, dist_eq_norm] at hs\n    exact hs\n  filter_upwards [hA.filter_mono nhdsWithin_le_nhds, self_mem_nhdsWithin,\n    h0.filter_mono nhdsWithin_le_nhds, hnorm.filter_mono nhdsWithin_le_nhds]\n    with s hAs hs1 h0s hsn\n  refine ⟨?_, h0s, fun n hn1 habs => ?_⟩\n  · intro hζ\n    rw [zetaA_apply hs1, hζ, mul_zero] at hAs\n    exact hAs rfl\n  · rw [habs] at hsn\n    have hnorm2 : ‖(-2 : ℂ) * (n : ℂ) - 1‖ = 2 * (n : ℝ) + 1 := by\n      have e : (-2 : ℂ) * (n : ℂ) - 1 = ((- (2 * (n : ℝ) + 1) : ℝ) : ℂ) := by\n        push_cast\n        ring\n      rw [e, Complex.norm_real, Real.norm_eq_abs, abs_neg, abs_of_nonneg (by\n        have hn0 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg _\n        linarith)]\n      ring\n    rw [hnorm2] at hsn\n    have hn1' : (1 : ℝ) ≤ (n : ℝ) := Nat.one_le_cast.mpr hn1\n    linarith\n\n/-- gFun(0) = B (punctured continuity; seriesFun(0) = 0). -/\nlemma gFun_zero (hZC : ZeroCountProp) : gFun 0 = momentB hZC := by\n  have hgood : ∀ᶠ s in 𝓝[≠] (0 : ℂ), gFun s = momentB hZC + seriesFun s := by\n    filter_upwards [good_eventually_zero, self_mem_nhdsWithin] with s ⟨hζ, h1, hn⟩ h0\n    exact gFun_eq_momentB hZC hζ h0 h1 hn\n  have hF : ContinuousAt gFun 0 := gFun_continuousAt 0 (by rw [xiL_zero]; norm_num)\n  have hG : ContinuousAt (fun s => momentB hZC + seriesFun s) 0 :=\n    continuousAt_const.add (seriesFun_analyticAt not_isNontrivialZero_zero).continuousAt\n  have h := eq_of_eventuallyEq_nhd_ne hF hG hgood\n  rwa [seriesFun_zero, add_zero] at h\n\n/-- gFun(1) = B + seriesFun(1) (punctured continuity). -/\nlemma gFun_one (hZC : ZeroCountProp) : gFun 1 = momentB hZC + seriesFun 1 := by\n  have hgood : ∀ᶠ s in 𝓝[≠] (1 : ℂ), gFun s = momentB hZC + seriesFun s := by\n    filter_upwards [good_eventually_one, self_mem_nhdsWithin] with s ⟨hζ, h0, hn⟩ h1\n    exact gFun_eq_momentB hZC hζ h0 h1 hn\n  have hF : ContinuousAt gFun 1 := gFun_continuousAt 1 (by rw [xiL_one]; norm_num)\n  have hG : ContinuousAt (fun s => momentB hZC + seriesFun s) 1 :=\n    continuousAt_const.add (seriesFun_analyticAt not_isNontrivialZero_one).continuousAt\n  exact eq_of_eventuallyEq_nhd_ne hF hG hgood\n\n/-- The FE sign: gFun(1) = −gFun(0) (xiL(1−s) = xiL(s), chain rule). -/\nlemma gFun_one_eq_neg : gFun 1 = -gFun 0 := by\n  have hfun : (fun s : ℂ => xiL (1 - s)) = xiL := funext xiL_one_sub\n  have hderiv : deriv (fun s : ℂ => xiL (1 - s)) 0 = -deriv xiL 1 := by\n    have h1 : DifferentiableAt ℂ xiL ((fun s : ℂ => 1 - s) 0) := by\n      simpa using differentiable_xiL 1\n    have h2 : DifferentiableAt ℂ (fun s : ℂ => 1 - s) 0 :=\n      (differentiableAt_const (1 : ℂ)).sub differentiableAt_id\n    have hcomp : deriv (xiL ∘ fun s : ℂ => 1 - s) 0 =\n        deriv (fun s : ℂ => 1 - s) 0 * deriv xiL ((fun s : ℂ => 1 - s) 0) :=\n      deriv.comp 0 h1 h2\n    have heq : (xiL ∘ fun s : ℂ => 1 - s) = fun s : ℂ => xiL (1 - s) := rfl\n    rw [heq] at hcomp\n    have hinner : deriv (fun s : ℂ => 1 - s) 0 = -1 := by\n      rw [deriv_const_sub differentiableAt_id]\n      simp\n    rw [hinner] at hcomp\n    simp at hcomp\n    exact hcomp\n  have h0 : deriv xiL 0 = -deriv xiL 1 := by\n    rw [← hfun]\n    exact hderiv\n  rw [gFun, gFun, logDeriv_apply, logDeriv_apply, xiL_zero, xiL_one, h0]\n  field_simp\n  ring\n\nend NguyenRH1\n"},"extra_content":null}]