← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (3098 chars)
Wait — the algebra at the end of iteratedDeriv_neg_zpow_neg_one_add is getting messy with the sign/exponent handling. Let me reconsider the target form.
The claim: iteratedDeriv k (fun s => −(s+c)^{−1}) s = −(−1)^k·k!·(s+c)^{−(k+1)}.
The step: the k+1 case: deriv of −(−1)^k·k!·(s+c)^{−(k+1)} = −(−1)^k·k!·(−(k+1))·(s+c)^{−(k+2)} — and the target: −(−1)^{k+1}·(k+1)!·(s+c)^{−(k+2)}. Check: −(−1)^k·(−(k+1)) = (−1)^k(k+1) = −(−1)^{k+1}(k+1) ✓ since −(−1)^{k+1} = (−1)^k ✓. So the goal: −(−1)^k·k!·((−(k+1):ℤ):ℂ)·(s+c)^{−(k+2)} = −(−1)^{k+1}·(k+1)!·(s+c)^{−(k+2)}.
The exponent forms: my statement uses `(-(k : ℤ) - 1)` for the k-th — so at k+1: `(-((k+1:ℕ):ℤ) - 1)` = −(k+1)−1 = −k−2 ✓ and the deriv's exponent: (−(k:ℤ)−1) − 1 = −k−2 ✓ same value, different expression — hexp bridges.
My ending block is convoluted. Let me simplify: after rw [h4] the goal is:
−(−1)^k·↑(k!)·((−(k:ℤ)−1:ℤ):ℂ)·(s+c)^(−(k:ℤ)−1−1) = −(−1)^{k+1}·↑((k+1)!)·(s+c)^(−((k+1:ℕ):ℤ)−1)
Both exponents equal −k−2 (as ℤ): rewrite both to a canonical form via hexp on both sides... hmm — rw [hexp] only rewrites the LHS's exponent. Let me instead just: convert everything with push_cast and ring_nf — the exponents are INSIDE zpow atoms — ring_nf won't equate zpow atoms with different exponent EXPRESSIONS even if equal... — need the exponents syntactically equal first. Let me handle:
```lean
rw [h4]
have hexp1 : (-(k : ℤ) - 1 - 1 : ℤ) = (-(k : ℤ) - 2 : ℤ) := by ring
have hexp2 : (-((k + 1 : ℕ) : ℤ) - 1 : ℤ) = (-(k : ℤ) - 2 : ℤ) := by push_cast; ring
rw [hexp1, hexp2]
-- now: −(−1)^k·↑k!·((−(k:ℤ)−1:ℤ):ℂ)·X = −(−1)^{k+1}·↑((k+1)!)·X with X := (s+c)^(−(k:ℤ)−2)
have hconst : ((-(k : ℤ) - 1 : ℤ) : ℂ) = -((k : ℂ) + 1) := by push_cast; ring
rw [hconst, hfact] -- hfact : ((k+1)!:ℂ) = (k+1)·(k!:ℂ)
rw [pow_succ] -- (−1)^{k+1} → (−1)^k·(−1)
ring
```
After these: LHS: −(−1)^k·↑k!·(−(↑k+1))·X; RHS: −((−1)^k·(−1))·((↑k+1)·↑k!)·X — ring: LHS = (−1)^k·↑k!·(↑k+1)·X·(−1)·(−1)... let me just verify ring can: LHS = −A·B·(−(k+1))·X = A·B·(k+1)·X where A := (−1)^k, B := ↑k!. RHS = −(A·(−1))·((k+1)·B)·X = A·(k+1)·B·X ✓ equal by comm ✓ ring closes ✓.
But careful about hfact's rewrite direction and the RHS's factorial form: the goal's RHS has `↑((k+1)!)` — hmm — the statement's (k+1) case: `(k + 1) !` cast — `((k + 1) ! : ℂ)` — hfact : ((k+1)!:ℂ) = (↑k+1)·(↑k!... — hmm my hfact was ((k + 1 : ℕ) ! : ℂ) = (k + 1) * (k ! : ℂ) — via Nat.factorial_succ: (k+1)! = (k+1)·k! — push_cast... — hmm — Nat.factorial_succ : (n+1)! = (n+1) * n! ✓ then casts — let me write hfact as:
```lean
have hfact : (((k + 1) ! : ℕ) : ℂ) = ((k : ℂ) + 1) * (k ! : ℂ) := by
rw [Nat.factorial_succ]
push_cast
ring -- ↑(k+1)·↑(k!) = (↑k+1)·↑k! — cast of (k+1) — push_cast ✓
```
Hmm — Nat.factorial_succ : (k+1)! = (k+1) * k! — the cast: ↑((k+1)·k!) — push_cast → (↑(k+1))·↑(k!) → (↑k+1)·↑k! ✓ — and the target (↑k+1)·↑k! — ring ✓ — actually after push_cast it should be syntactic — `ring` safe.
Let me rewrite the whole ending block of the zpow lemma cleanly. Replace from `have hfact` onward.
The ending algebra of the zpow lemma is convoluted — rewriting it cleanly.
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
"old_string": " rw [h4]\n -- algebra: the constants and the exponent\n have hfact : ((k + 1 : \u2115) ! : \u2102) = (k + 1) * (k ! : \u2102) := by\n rw [Nat.factorial_succ]\n push_cast\n ring\n have hexp : (-(k : \u2124) - 1 - 1 : \u2124) = (-((k + 1 : \u2115) : \u2124) - 1 : \u2124) := by\n push_cast\n ring\n have hsign : -((-1 : \u2102)) ^ (k + 1) = -((-1 : \u2102)) ^ k * -((-(k : \u2124) - 1 : \u2124) : \u2102) := by\n rw [pow_succ]\n push_cast\n ring\n rw [hexp, hfact]\n rw [hsign]\n ring_nf\n -- reconcile -(\u22121)^k\u00b7k!\u00b7((\u2212(k+1))\u00b7X) with the two forms\n have h5 : (((-(k : \u2124) - 1 : \u2124) : \u2102)) = -((k : \u2102) + 1) := by push_cast; ring\n rw [h5]\n ring",
"new_string": " rw [h4]\n -- normalize the exponents to \u2212(k:\u2124)\u22122, then the constants\n have hexp1 : (-(k : \u2124) - 1 - 1 : \u2124) = (-(k : \u2124) - 2 : \u2124) := by ring\n have hexp2 : (-((k + 1 : \u2115) : \u2124) - 1 : \u2124) = (-(k : \u2124) - 2 : \u2124) := by push_cast; ring\n rw [hexp1, hexp2]\n have hconst : ((-(k : \u2124) - 1 : \u2124) : \u2102) = -((k : \u2102) + 1) := by push_cast; ring\n have hfact : (((k + 1) ! : \u2115) : \u2102) = ((k : \u2102) + 1) * (k ! : \u2102) := by\n rw [Nat.factorial_succ]\n push_cast\n ring\n rw [hconst, hfact, pow_succ]\n ring"
}
result 2026-08-22 08:17:50Z → 2026-08-23 19:43:45Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean",
"oldString": " have hmax : max |-(2 : \u211d) ^ (j + 1) * X| |-(2 : \u211d) ^ j * X|\n \u2264 (2 : \u211d) ^ (j + 1) * X := by\n apply max_le\n \u00b7 rw [abs_neg, abs_of_nonneg h2j1X.le]\n \u00b7 rw [abs_neg, abs_of_nonneg h2jX.le]\n nlinarith [h2jX, h2j1X]",
"newString": " have hmax : max |-(2 : \u211d) ^ (j + 1) * X| |-(2 : \u211d) ^ j * X|\n \u2264 (2 : \u211d) ^ (j + 1) * X := by\n apply max_le\n \u00b7 rw [neg_mul, abs_neg, abs_of_nonneg h2j1X.le]\n \u00b7 rw [neg_mul, abs_neg, abs_of_nonneg h2jX.le]\n nlinarith [h2jX, h2j1X]",
"originalFile": "/-\nNguyenRH1/LiCircleBound.lean \u2014 tier ii\u2032 sub-stage ii\u2032-5e-v (D-068 \u00a75):\nthe circle bound for the partial-fraction difference and the squeeze to\nthe capstone identity.\n\n\u00a70: conjugate symmetry of the nontrivial zeros (for the lower-half\n circle arcs).\n\u00a71: the mult-weighted ordinate-window count bridges from Zeta23's RvM\n local count (`zeta_local_zero_count`: Ncount(t, t+1] \u2264 A\u2080\u00b7log(|t|+3)\n with multiplicity, ALL t \u2014 no perimeter): `A0count` + the dyadic\n interval count `Ncount_le_of_interval`.\n\u00a72: the Dirichlet bound `norm_logDeriv_zeta_le_dirichlet` (\u2016\u03b6\u2032/\u03b6 s\u2016 \u2264\n dirichletC2 for re s \u2265 2; \u2212\u03b6\u2032/\u03b6 = LSeries \u039b, termwise \u2264 the s = 2\n majorant) \u2014 the right near-axis arc input.\n\u00a73+: (this file, subsequent sub-stages) the series bound, the logDeriv\n assembly, the Fexpr circle bound, the Schwarz squeeze, and the\n capstone `partialFraction_identity`.\n\nArchive references: D-068 \u00a75, journal-029.\n-/\nimport Mathlib\nimport Zeta23.RvM.LocalCount\nimport NguyenRH1.LiFEntire\nimport NguyenRH1.LiGapCircles\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 0. Conjugate symmetry -/\n\n/-- The conjugate of a nontrivial zero is a nontrivial zero. -/\nlemma isNontrivialZero_conj {\u03c1 : \u2102} (h\u03c1 : IsNontrivialZero \u03c1) :\n IsNontrivialZero ((starRingEnd \u2102) \u03c1) := by\n refine \u27e8?_, ?_, ?_\u27e9\n \u00b7 rw [_root_.riemannZeta_conj, h\u03c1.1, map_zero]\n \u00b7 rw [Complex.conj_re]; exact h\u03c1.2.1\n \u00b7 rw [Complex.conj_re]; exact h\u03c1.2.2\n\n/-! ## 1. The mult-weighted window count bridges -/\n\n/-- The local-count constant: from Zeta23's RvM local count\n(`zeta_local_zero_count`, [Tit86 Thm 9.2] \u2014 mult-weighted, two-sided,\nall t, PROVED unconditionally in Zeta23). -/\ndef A0count : \u211d := Classical.choose Zeta23.RvM.zeta_local_zero_count\n\nlemma A0count_ge_one : (1 : \u211d) \u2264 A0count :=\n (Classical.choose_spec Zeta23.RvM.zeta_local_zero_count).1\n\nlemma A0count_pos : (0 : \u211d) < A0count := lt_of_lt_of_le one_pos A0count_ge_one\n\n/-- The unit-window bound: Ncount(t, t+1] \u2264 A\u2080\u00b7log(|t|+3). -/\nlemma Ncount_window_le (t : \u211d) :\n (Zeta23.Ncount t (t + 1) : \u211d) \u2264 A0count * Real.log (|t| + 3) :=\n (Classical.choose_spec Zeta23.RvM.zeta_local_zero_count).2 t\n\n/-- Window additivity: Ncount(a, c] = Ncount(a, b] + Ncount(b, c] for\na \u2264 b \u2264 c (the disjoint union of the ordinate windows). -/\nlemma Ncount_add_of_le {a b c : \u211d} (hab : a \u2264 b) (hbc : b \u2264 c) :\n Zeta23.Ncount a c = Zeta23.Ncount a b + Zeta23.Ncount b c := by\n have hunion : Zeta23.zerosIn a c = Zeta23.zerosIn a b \u222a Zeta23.zerosIn b c := by\n ext \u03c1\n constructor\n \u00b7 intro h\u03c1c\n obtain \u27e8h\u03c1, ha, hc\u27e9 := h\u03c1c\n rcases le_or_gt \u03c1.im b with h | h\n \u00b7 exact Set.mem_union_left _ \u27e8h\u03c1, ha, h\u27e9\n \u00b7 exact Set.mem_union_right _ \u27e8h\u03c1, h, hc\u27e9\n \u00b7 intro h\n rcases h with h\u03c1b | h\u03c1c\n \u00b7 obtain \u27e8h\u03c1, ha, hb\u27e9 := h\u03c1b\n exact \u27e8h\u03c1, ha, hb.trans hbc\u27e9\n \u00b7 obtain \u27e8h\u03c1, hb, hc\u27e9 := h\u03c1c\n exact \u27e8h\u03c1, hab.trans_lt hb, hc\u27e9\n have hdisj : Disjoint (Zeta23.zerosIn a b) (Zeta23.zerosIn b c) := by\n rw [Set.disjoint_iff]\n intro \u03c1 \u27e8h1, h2\u27e9\n exact absurd (h1.2.2.trans_lt h2.2.1) (lt_irrefl \u03c1.im)\n rw [Zeta23.Ncount, Zeta23.Ncount, Zeta23.Ncount, hunion]\n exact_mod_cast finsum_mem_union hdisj (Zeta23.zerosIn_finite a b)\n (Zeta23.zerosIn_finite b c)\n\n/-- The N-step unit-window chain: Ncount(a, a+N] \u2264 A\u2080\u00b7N\u00b7log(|a|+N+3). -/\nlemma Ncount_chain_le (a : \u211d) (N : \u2115) :\n (Zeta23.Ncount a (a + (N : \u211d)) : \u211d)\n \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := by\n induction N with\n | zero =>\n simp only [Nat.cast_zero, add_zero]\n have h0 : Zeta23.zerosIn a a = \u2205 := by\n ext \u03c1\n constructor\n \u00b7 intro h\n obtain \u27e8-, h1, h2\u27e9 := h\n exact absurd (h2.trans_lt h1) (lt_irrefl _)\n \u00b7 intro h\n simp at h\n have hz : Zeta23.Ncount a a = 0 := by\n simp only [Zeta23.Ncount, h0, finsum_mem_empty]\n rw [hz, Nat.cast_zero]\n simp\n | succ N ih =>\n have hN0 : (0 : \u211d) \u2264 (N : \u211d) := Nat.cast_nonneg N\n have hsplit : Zeta23.Ncount a (a + (N : \u211d) + 1)\n = Zeta23.Ncount a (a + (N : \u211d)) + Zeta23.Ncount (a + (N : \u211d)) (a + (N : \u211d) + 1) :=\n Ncount_add_of_le (a := a) (b := a + (N : \u211d)) (c := a + (N : \u211d) + 1)\n (by linarith) (by linarith)\n have hcast : a + ((N + 1 : \u2115) : \u211d) = a + (N : \u211d) + 1 := by push_cast; ring\n rw [hcast, hsplit]\n have hwin := Ncount_window_le (a + (N : \u211d))\n have hlog : Real.log (|a + (N : \u211d)| + 3) \u2264 Real.log (|a| + (N : \u211d) + 3) := by\n apply Real.log_le_log (by positivity)\n have h1 : |a + (N : \u211d)| \u2264 |a| + (N : \u211d) :=\n (abs_add_le _ _).trans (by rw [abs_of_nonneg (show (0 : \u211d) \u2264 (N : \u211d) from Nat.cast_nonneg N)])\n linarith\n have hlogpos : (0 : \u211d) \u2264 Real.log (|a| + (N : \u211d) + 3) := by\n apply Real.log_nonneg\n have h1 : (1 : \u211d) \u2264 |a| + 3 := by linarith [abs_nonneg a]\n linarith [hN0]\n have hlogpos' : (0 : \u211d) \u2264 Real.log (|a| + ((N : \u211d) + 1) + 3) := by\n apply Real.log_nonneg\n have h1 : (1 : \u211d) \u2264 |a| + 3 := by linarith [abs_nonneg a]\n linarith [hN0]\n push_cast\n -- goal: \u2191(Ncount a (a+\u2191N)) + \u2191(Ncount (a+\u2191N) (a+\u2191N+1)) \u2264 A\u2080(\u2191N+1)\u00b7log(|a|+(\u2191N+1)+3)\n have hlogC : Real.log (|a| + (N : \u211d) + 3)\n \u2264 Real.log (|a| + ((N : \u211d) + 1) + 3) :=\n Real.log_le_log (by positivity) (by linarith)\n have hle1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n \u2264 A0count * (N : \u211d) * Real.log (|a| + ((N : \u211d) + 1) + 3) :=\n mul_le_mul_of_nonneg_left hlogC (mul_nonneg A0count_pos.le hN0)\n have hle2 : A0count * Real.log (|a + (N : \u211d)| + 3)\n \u2264 A0count * Real.log (|a| + ((N : \u211d) + 1) + 3) := by\n apply mul_le_mul_of_nonneg_left _ A0count_pos.le\n apply Real.log_le_log (by positivity)\n have h1 : |a + (N : \u211d)| \u2264 |a| + (N : \u211d) :=\n (abs_add_le _ _).trans (by rw [abs_of_nonneg (show (0 : \u211d) \u2264 (N : \u211d) from Nat.cast_nonneg N)])\n linarith\n have hsum : \u2191(Zeta23.Ncount a (a + (N : \u211d))) + \u2191(Zeta23.Ncount (a + (N : \u211d)) (a + (N : \u211d) + 1))\n \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n + A0count * Real.log (|a + (N : \u211d)| + 3) :=\n add_le_add ih hwin\n linarith [hsum, hle1, hle2]\n\n/-- The dyadic-interval count: Ncount(a, b] \u2264 A\u2080\u00b7(b\u2212a+1)\u00b7log(b+4) for\n0 \u2264 a \u2264 b (the unit-window chain + the ceil cover). -/\nlemma Ncount_le_of_interval {a b : \u211d} (ha : 0 \u2264 a) (hab : a \u2264 b) :\n (Zeta23.Ncount a b : \u211d) \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n set N : \u2115 := \u2308b - a\u2309\u208a with hN\n have hNb : b \u2264 a + (N : \u211d) := by\n have h := Nat.le_ceil (b - a)\n rw [\u2190 hN] at h\n have h2 : (b - a : \u211d) \u2264 (N : \u211d) := h\n linarith\n have hsub : Zeta23.zerosIn a b \u2286 Zeta23.zerosIn a (a + (N : \u211d)) := by\n intro \u03c1 h\u03c1\n refine \u27e8h\u03c1.1, h\u03c1.2.1, ?_\u27e9\n exact h\u03c1.2.2.trans hNb\n have hle : Zeta23.Ncount a b \u2264 Zeta23.Ncount a (a + (N : \u211d)) := by\n rw [Zeta23.Ncount, Zeta23.Ncount]\n rw [finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a b),\n finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a (a + (N : \u211d)))]\n apply Finset.sum_le_sum_of_subset_of_nonneg\n \u00b7 intro \u03c1 h\u03c1\n rw [Set.Finite.mem_toFinset] at h\u03c1 \u22a2\n exact hsub h\u03c1\n \u00b7 intro \u03c1 _ _\n exact Nat.cast_nonneg _\n have hchain := Ncount_chain_le a N\n have hNle : (N : \u211d) \u2264 b - a + 1 := by\n have h := Nat.ceil_lt_add_one (sub_nonneg.mpr hab)\n rw [\u2190 hN] at h\n have h2 : ((N : \u211d)) < b - a + 1 := by exact_mod_cast h\n linarith\n have hlogle : Real.log (|a| + (N : \u211d) + 3) \u2264 Real.log (b + 4) := by\n apply Real.log_le_log (by positivity)\n rw [abs_of_nonneg ha]\n linarith\n calc (Zeta23.Ncount a b : \u211d)\n \u2264 (Zeta23.Ncount a (a + (N : \u211d)) : \u211d) := by exact_mod_cast hle\n _ \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := hchain\n _ \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n have hlogpos : (0 : \u211d) \u2264 Real.log (b + 4) := by\n apply Real.log_nonneg; linarith\n have h1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n \u2264 A0count * (N : \u211d) * Real.log (b + 4) :=\n mul_le_mul_of_nonneg_left hlogle (mul_nonneg A0count_pos.le (Nat.cast_nonneg N))\n have h2 : A0count * (N : \u211d) * Real.log (b + 4)\n \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n apply mul_le_mul_of_nonneg_right _ hlogpos\n nlinarith [A0count_pos, hNle, sub_nonneg.mpr hab]\n exact h1.trans h2\n\n/-! ## 2. The Dirichlet bound -/\n\n/-- The Dirichlet majorant constant: the absolute sum of the von\nMangoldt L-series terms at s = 2 (summable since 2 > 1). -/\ndef dirichletC2 : \u211d :=\n \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 C\u2082 for re s \u2265 2 (the Dirichlet-series majorant:\n\u2212\u03b6\u2032/\u03b6 = LSeries \u039b for re > 1, termwise \u2264 the s = 2 sum). -/\nlemma norm_logDeriv_zeta_le_dirichlet {s : \u2102} (hs : 2 \u2264 s.re) :\n \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC2 := by\n have hs1 : (1 : \u211d) < s.re := by linarith\n have h1 : -logDeriv riemannZeta s\n = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s := by\n have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n rw [logDeriv, Pi.div_apply, h2]\n ring\n have hsum2 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsumS : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016\n \u2264 dirichletC2 := by\n show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 \u2264 _\n calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016\n \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 :=\n norm_tsum_le_tsum_norm hsumS\n _ \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n simp\n exact hs) n) hsumS hsum2\n _ = dirichletC2 := rfl\n calc \u2016logDeriv riemannZeta s\u2016\n = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016 := by\n rw [\u2190 h1, norm_neg]\n _ \u2264 dirichletC2 := hle\n\n/-! ## 3. The tsum split + the generalized interval count + the low-zero\nconstant -/\n\n/-- Splitting a summable real tsum over a finset:\n\u2211' f = \u2211_{i \u2208 s} f i + \u2211' (if i \u2208 s then 0 else f i). -/\nlemma tsum_split_finset {\u03b9 : Type*} [DecidableEq \u03b9] {f : \u03b9 \u2192 \u211d} (hf : Summable f)\n (s : Finset \u03b9) :\n \u2211' i, f i = \u2211 i \u2208 s, f i + \u2211' i, (if i \u2208 s then 0 else f i) := by\n classical\n have h1 : Summable (fun i => if i \u2208 s then f i else 0) := by\n apply Summable.of_norm_bounded hf.norm\n intro i\n by_cases hi : i \u2208 s <;> simp [hi]\n have h2 : Summable (fun i => if i \u2208 s then 0 else f i) := by\n apply Summable.of_norm_bounded hf.norm\n intro i\n by_cases hi : i \u2208 s <;> simp [hi]\n have h3 : \u2211' i, f i\n = \u2211' i, ((if i \u2208 s then f i else 0) + (if i \u2208 s then 0 else f i)) := by\n apply tsum_congr\n intro i\n by_cases hi : i \u2208 s <;> simp [hi]\n rw [h3, Summable.tsum_add h1 h2]\n congr 1\n rw [tsum_eq_sum (s := s) (fun b hb => if_neg hb)]\n exact Finset.sum_congr rfl (fun b hb => if_pos hb)\n\n/-- The generalized dyadic-interval count (both signs):\nNcount(a, b] \u2264 A\u2080\u00b7(b\u2212a+1)\u00b7log(3\u00b7max|a||b| + 5). -/\nlemma Ncount_le_of_interval_gen {a b : \u211d} (hab : a \u2264 b) :\n (Zeta23.Ncount a b : \u211d)\n \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n set N : \u2115 := \u2308b - a\u2309\u208a with hN\n have hNb : b \u2264 a + (N : \u211d) := by\n have h := Nat.le_ceil (b - a)\n rw [\u2190 hN] at h\n linarith\n have hsub : Zeta23.zerosIn a b \u2286 Zeta23.zerosIn a (a + (N : \u211d)) := by\n intro \u03c1 h\u03c1\n exact \u27e8h\u03c1.1, h\u03c1.2.1, h\u03c1.2.2.trans hNb\u27e9\n have hle : Zeta23.Ncount a b \u2264 Zeta23.Ncount a (a + (N : \u211d)) := by\n rw [Zeta23.Ncount, Zeta23.Ncount]\n rw [finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a b),\n finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a (a + (N : \u211d)))]\n apply Finset.sum_le_sum_of_subset_of_nonneg\n \u00b7 intro \u03c1 h\u03c1\n rw [Set.Finite.mem_toFinset] at h\u03c1 \u22a2\n exact hsub h\u03c1\n \u00b7 intro \u03c1 _ _\n exact Nat.cast_nonneg _\n have hchain := Ncount_chain_le a N\n have hNle : (N : \u211d) \u2264 b - a + 1 := by\n have h := Nat.ceil_lt_add_one (sub_nonneg.mpr hab)\n rw [\u2190 hN] at h\n have h2 : ((N : \u211d)) < b - a + 1 := by exact_mod_cast h\n linarith\n have hlogle : Real.log (|a| + (N : \u211d) + 3)\n \u2264 Real.log (3 * max |a| |b| + 5) := by\n apply Real.log_le_log (by positivity)\n have hM1 : |a| \u2264 max |a| |b| := le_max_left _ _\n have hM2 : |b| \u2264 max |a| |b| := le_max_right _ _\n have hba : b - a \u2264 |b| + |a| := by\n have h1 := le_abs_self b\n have h2 : -a \u2264 |a| := by rw [\u2190 abs_neg a]; exact le_abs_self (-a)\n linarith\n nlinarith [hNle, hM1, hM2, hba, abs_nonneg a, abs_nonneg b]\n have hlogpos : (0 : \u211d) \u2264 Real.log (3 * max |a| |b| + 5) := by\n apply Real.log_nonneg\n have h1 : (0 : \u211d) \u2264 max |a| |b| := le_trans (abs_nonneg a) (le_max_left _ _)\n linarith\n calc (Zeta23.Ncount a b : \u211d)\n \u2264 (Zeta23.Ncount a (a + (N : \u211d)) : \u211d) := by exact_mod_cast hle\n _ \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := hchain\n _ \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n have h1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n \u2264 A0count * (N : \u211d) * Real.log (3 * max |a| |b| + 5) :=\n mul_le_mul_of_nonneg_left hlogle (mul_nonneg A0count_pos.le (Nat.cast_nonneg N))\n have h2 : A0count * (N : \u211d) * Real.log (3 * max |a| |b| + 5)\n \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n apply mul_le_mul_of_nonneg_right _ hlogpos\n nlinarith [A0count_pos, hNle, sub_nonneg.mpr hab]\n exact h1.trans h2\n\n/-- The low-zero finset: nontrivial zeros with \u2016\u03c1\u2016 \u2264 3. -/\ndef lowZeros : Finset {\u03c1 : \u2102 // IsNontrivialZero \u03c1} :=\n (show {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | \u2016(\u03c1 : \u2102)\u2016 \u2264 3}.Finite from\n (finite_subtype_norm_lt 4).subset\n (fun \u03c1 h\u03c1 => lt_of_le_of_lt (show \u2016(\u03c1 : \u2102)\u2016 \u2264 3 from h\u03c1) (by norm_num))).toFinset\n\n/-- The low-zero symbolic constant (a fixed finite sum of fixed positive\nreals; \u2016\u03c1\u2016 > 0 for nontrivial \u03c1 since re \u03c1 > 0). -/\ndef lowZeroConst : \u211d :=\n \u2211 \u03c1 \u2208 lowZeros, (zeroMult (\u03c1 : \u2102) : \u211d) * (1 + 1 / \u2016(\u03c1 : \u2102)\u2016)\n\nlemma lowZeroConst_nonneg : 0 \u2264 lowZeroConst :=\n Finset.sum_nonneg fun _\u03c1 _ => mul_nonneg (Nat.cast_nonneg _)\n (add_nonneg one_pos.le (div_nonneg one_pos.le (norm_nonneg _)))\n\n/-! ## 4. The far-tail bound -/\n\n/-- The dyadic log series closed form:\n\u2211' j, ((j+4)\u00b7log 2 + log X)/2^j = 10\u00b7log 2 + 2\u00b7log X. -/\nlemma tsum_dyadic_log (X : \u211d) :\n \u2211' j : \u2115, ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j\n = 10 * Real.log 2 + 2 * Real.log X := by\n have hgeom2H : Summable (fun j : \u2115 => ((1 : \u211d) / 2) ^ j) := summable_geometric_two\n have hgeom2 : \u2211' j : \u2115, ((1 : \u211d) / 2) ^ j = 2 := tsum_geometric_two\n have hlinH := hasSum_coe_mul_geometric_of_norm_lt_one (r := (1 : \u211d) / 2) (by norm_num)\n have hlin : \u2211' j : \u2115, (j : \u211d) * ((1 : \u211d) / 2) ^ j = 2 := by\n have h := hlinH.tsum_eq\n norm_num at h\n exact h\n have hsplit : (fun j : \u2115 => ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j)\n = fun j : \u2115 => Real.log 2 * ((j : \u211d) * ((1 : \u211d) / 2) ^ j)\n + (4 * Real.log 2 + Real.log X) * ((1 : \u211d) / 2) ^ j := by\n funext j\n have hj : (2 : \u211d) ^ j \u2260 0 := pow_ne_zero _ two_ne_zero\n rw [one_div_pow]\n field_simp\n ring\n rw [hsplit, Summable.tsum_add (hlinH.summable.mul_left _) (hgeom2H.mul_left _)]\n rw [tsum_mul_left, tsum_mul_left, hlin, hgeom2]\n ring\n\n/-- log 2 \u2264 1 (since 2 \u2264 e). -/\nlemma log_two_le_one : Real.log 2 \u2264 1 := by\n rw [show (1 : \u211d) = Real.log (Real.exp 1) by rw [Real.log_exp]]\n apply Real.log_le_log (by norm_num)\n have h := Real.exp_one_gt_d9\n linarith\n\n/-- For X \u2265 200: (4A\u2080/X)\u00b7(10\u00b7log 2 + 2\u00b7log X) \u2264 16\u00b7A\u2080\u00b7log X / X. -/\nlemma dyadic_tail_constant {X : \u211d} (hX : 200 \u2264 X) :\n (4 * A0count / X) * (10 * Real.log 2 + 2 * Real.log X)\n \u2264 16 * A0count * Real.log X / X := by\n have hX0 : (0 : \u211d) < X := by linarith\n have hlogX : 5 \u2264 Real.log X := by\n rw [show (5 : \u211d) = Real.log (Real.exp 5) by rw [Real.log_exp]]\n apply Real.log_le_log (Real.exp_pos _)\n have h1 : Real.exp 5 = (Real.exp 1) ^ 5 := by\n rw [\u2190 Real.exp_nat_mul]\n norm_num\n have h2 := Real.exp_one_lt_d9.le\n have h3 : (Real.exp 1) ^ 5 \u2264 (2.7182818286 : \u211d) ^ 5 :=\n pow_le_pow_left\u2080 (Real.exp_pos 1).le h2 5\n have h4 : (2.7182818286 : \u211d) ^ 5 \u2264 200 := by norm_num\n linarith [h1, h3, h4]\n have hlog2 := log_two_le_one\n have hA0 : (0 : \u211d) \u2264 4 * A0count / X :=\n div_nonneg (mul_nonneg (by norm_num) A0count_pos.le) hX0.le\n have h1 : 10 * Real.log 2 + 2 * Real.log X \u2264 4 * Real.log X := by linarith\n calc (4 * A0count / X) * (10 * Real.log 2 + 2 * Real.log X)\n \u2264 (4 * A0count / X) * (4 * Real.log X) := mul_le_mul_of_nonneg_left h1 hA0\n _ = 16 * A0count * Real.log X / X := by ring\n\n/-- The dyadic class of a zero relative to scale X:\nNat.log 2 \u230a|im \u03c1|/X\u230b\u208a, so 2^j\u00b7X \u2264 |im \u03c1| < 2^{j+1}\u00b7X when |im \u03c1| \u2265 X. -/\ndef dyadClass (X : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2115 :=\n Nat.log 2 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a\n\nlemma dyadClass_lower {X : \u211d} (hX : 0 < X) {\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}}\n (h\u03c1 : X \u2264 |(\u03c1 : \u2102).im|) :\n (2 : \u211d) ^ dyadClass X \u03c1 * X \u2264 |(\u03c1 : \u2102).im| := by\n have hfl : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a \u2260 0 := by\n rw [Ne, Nat.floor_eq_zero]\n push Not\n have h1 : (1 : \u211d) \u2264 |(\u03c1 : \u2102).im| / X := (le_div_iff\u2080 hX).mpr (by linarith)\n linarith\n have h2 := Nat.pow_log_le_self 2 hfl\n have h3 : ((2 ^ dyadClass X \u03c1 : \u2115) : \u211d) \u2264 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a := by exact_mod_cast h2\n have h4 : (\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a : \u211d) \u2264 |(\u03c1 : \u2102).im| / X := Nat.floor_le (by positivity)\n have h5 : ((2 ^ dyadClass X \u03c1 : \u2115) : \u211d) = (2 : \u211d) ^ dyadClass X \u03c1 := by push_cast; ring\n rw [h5] at h3\n rw [le_div_iff\u2080 hX] at h4\n have h6 : (2 : \u211d) ^ dyadClass X \u03c1 * X \u2264 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a * X :=\n mul_le_mul_of_nonneg_right h3 hX.le\n linarith\n\nlemma dyadClass_upper {X : \u211d} (hX : 0 < X) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n |(\u03c1 : \u2102).im| < (2 : \u211d) ^ (dyadClass X \u03c1 + 1) * X := by\n have h2 : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a < 2 ^ (dyadClass X \u03c1 + 1) :=\n Nat.lt_pow_succ_log_self (by norm_num) _\n have h3 : (\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a : \u211d) + 1 \u2264 (2 : \u211d) ^ (dyadClass X \u03c1 + 1) := by\n have h4 : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a + 1 \u2264 2 ^ (dyadClass X \u03c1 + 1) := h2\n have h5 : ((\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a + 1 : \u2115) : \u211d) \u2264 ((2 ^ (dyadClass X \u03c1 + 1) : \u2115) : \u211d) := by\n exact_mod_cast h4\n push_cast at h5\n linarith\n have h6 : |(\u03c1 : \u2102).im| / X < (2 : \u211d) ^ (dyadClass X \u03c1 + 1) :=\n (Nat.lt_floor_add_one _).trans_le h3\n rw [div_lt_iff\u2080 hX] at h6\n linarith\n\n/-- The tail summand (if-form on the zero subtype). -/\ndef tailTerm (X : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u211d :=\n if X < |(\u03c1 : \u2102).im| then (zeroMult \u03c1 : \u211d) / (1 + ((\u03c1 : \u2102).im) ^ 2) else 0\n\nlemma tailTerm_nonneg {X : \u211d} (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n 0 \u2264 tailTerm X \u03c1 := by\n by_cases h : X < |(\u03c1 : \u2102).im| <;>\n simp [tailTerm, h, div_nonneg (Nat.cast_nonneg _)\n (by positivity : (0 : \u211d) \u2264 1 + ((\u03c1 : \u2102).im) ^ 2)]\n\n/-- The tail summand is summable (dominated by 2\u00b7m/(1+\u2016\u03b3\u2016\u00b2) via\n1 + \u2016\u03b3\u2016\u00b2 \u2264 2(1 + im\u00b2)). -/\nlemma tailTerm_summable (X : \u211d) :\n Summable (tailTerm X) := by\n have hbase : Summable (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))) :=\n (WeilEF.zero_sum_inv_sq zetaSeam).mul_left 2\n apply Summable.of_norm_bounded hbase\n intro \u03c1\n rw [tailTerm]\n by_cases h : X < |(\u03c1 : \u2102).im|\n \u00b7 rw [if_pos h]\n have hgam : Complex.normSq (gammaOf (\u03c1 : \u2102))\n = (\u03c1 : \u2102).im ^ 2 + (1 / 2 - (\u03c1 : \u2102).re) ^ 2 := by\n rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]\n ring\n have hcmp : 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) \u2264 2 * (1 + (\u03c1 : \u2102).im ^ 2) := by\n rw [hgam]\n have hre : ((\u03c1 : \u2102).re - 1 / 2) ^ 2 \u2264 1 / 4 := by\n have h0 := \u03c1.2.2.1\n have h1 := \u03c1.2.2.2\n nlinarith [sq_nonneg ((\u03c1 : \u2102).re - 1 / 2)]\n nlinarith [sq_nonneg (\u03c1 : \u2102).im]\n have hpos1 : (0 : \u211d) < 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) := by\n have h := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102)); linarith\n have hpos2 : (0 : \u211d) < 1 + (\u03c1 : \u2102).im ^ 2 := by positivity\n have hfrac : 1 / (1 + (\u03c1 : \u2102).im ^ 2) \u2264 2 / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))) := by\n rw [div_le_div_iff\u2080 hpos2 hpos1]\n nlinarith [hcmp]\n have hm : (0 : \u211d) \u2264 (zeroMult \u03c1 : \u211d) := Nat.cast_nonneg _\n calc \u2016(zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)\u2016\n = (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2) := by\n rw [Real.norm_eq_abs, abs_of_nonneg (div_nonneg (Nat.cast_nonneg _) hpos2.le)]\n _ \u2264 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) := by\n rw [show (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)\n = (zeroMult \u03c1 : \u211d) * (1 / (1 + (\u03c1 : \u2102).im ^ 2)) from by ring]\n rw [show 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))\n = (zeroMult \u03c1 : \u211d) * (2 / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) from by ring]\n exact mul_le_mul_of_nonneg_left hfrac hm\n \u00b7 rw [if_neg h, norm_zero]\n have hnn := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102))\n exact mul_nonneg (by norm_num) (div_nonneg (Nat.cast_nonneg _) (by linarith))\n\n/-- The dyadic log series is summable. -/\nlemma dyadicLog_summable (X : \u211d) :\n Summable (fun j : \u2115 => ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j) := by\n have hlinH := hasSum_coe_mul_geometric_of_norm_lt_one (r := (1 : \u211d) / 2) (by norm_num)\n have hsplit : (fun j : \u2115 => ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j)\n = fun j : \u2115 => Real.log 2 * ((j : \u211d) * ((1 : \u211d) / 2) ^ j)\n + (4 * Real.log 2 + Real.log X) * ((1 : \u211d) / 2) ^ j := by\n funext j\n have hj : (2 : \u211d) ^ j \u2260 0 := pow_ne_zero _ two_ne_zero\n rw [one_div_pow]\n field_simp\n ring\n rw [hsplit]\n exact (hlinH.summable.mul_left _).add (summable_geometric_two.mul_left _)\n\n/-- The dyadic fiber {dyadClass X \u03c1 = j} is finite. -/\nlemma dyadClass_fiber_finite {X : \u211d} (hX : 0 < X) (j : \u2115) :\n {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | dyadClass X \u03c1 = j \u2227 X < |(\u03c1 : \u2102).im|}.Finite := by\n apply (finite_subtype_norm_lt (1 + (2 : \u211d) ^ (j + 1) * X + 1)).subset\n intro \u03c1 h\u03c1\n have h\u03c1j : dyadClass X \u03c1 = j := h\u03c1.1\n have hup := dyadClass_upper hX \u03c1\n rw [h\u03c1j] at hup\n have hnorm : \u2016(\u03c1 : \u2102)\u2016 \u2264 |(\u03c1 : \u2102).re| + |(\u03c1 : \u2102).im| :=\n Complex.norm_le_abs_re_add_abs_im _\n have hre : |(\u03c1 : \u2102).re| \u2264 1 := by\n rw [abs_le]\n exact \u27e8by linarith [\u03c1.2.2.1], by linarith [\u03c1.2.2.2]\u27e9\n have h2pow : (0 : \u211d) \u2264 (2 : \u211d) ^ (j + 1) * X := by positivity\n show \u2016(\u03c1 : \u2102)\u2016 < 1 + (2 : \u211d) ^ (j + 1) * X + 1\n linarith\n\n/-- The fiber count: the zeros in the dyadic fiber with X < |\u03b3| have\nmultiplicity-sum \u2264 A\u2080\u00b7(2^{j+1}X+3)\u00b7log(3\u00b72^{j+1}X+5). -/\nlemma fiber_mult_count {X : \u211d} (hX : 200 \u2264 X) (j : \u2115) :\n \u2211 \u03c1 \u2208 (dyadClass_fiber_finite (by linarith : (0 : \u211d) < X) j).toFinset,\n (zeroMult (\u03c1 : \u2102) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n classical\n have hX0 : (0 : \u211d) < X := by linarith\n have h2jX : (0 : \u211d) < (2 : \u211d) ^ j * X := by positivity\n have h2j1X : (0 : \u211d) < (2 : \u211d) ^ (j + 1) * X := by positivity\n set FS := (dyadClass_fiber_finite (by linarith : (0 : \u211d) < X) j).toFinset with hFS\n have hmemFS : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n \u03c1 \u2208 FS \u2194 dyadClass X \u03c1 = j \u2227 X < |(\u03c1 : \u2102).im| := by\n intro \u03c1\n rw [hFS, Set.Finite.mem_toFinset]\n exact Iff.rfl\n have hW1 : (Zeta23.zerosIn ((2 : \u211d) ^ j * X - 1) ((2 : \u211d) ^ (j + 1) * X)).Finite :=\n Zeta23.zerosIn_finite _ _\n have hW2 : (Zeta23.zerosIn (-(2 : \u211d) ^ (j + 1) * X) (-((2 : \u211d) ^ j * X))).Finite :=\n Zeta23.zerosIn_finite _ _\n have himg : FS.image (Subtype.val) \u2286 hW1.toFinset \u222a hW2.toFinset := by\n intro z hz\n obtain \u27e8\u03c1, h\u03c1, rfl\u27e9 := Finset.mem_image.mp hz\n rw [hmemFS] at h\u03c1\n obtain \u27e8h\u03c1j, hgt\u27e9 := h\u03c1\n have hup : |(\u03c1 : \u2102).im| < (2 : \u211d) ^ (j + 1) * X := by\n have h := dyadClass_upper hX0 \u03c1\n rw [h\u03c1j] at h\n exact h\n have hlo : (2 : \u211d) ^ j * X \u2264 |(\u03c1 : \u2102).im| := by\n have h := dyadClass_lower hX0 (show X \u2264 |(\u03c1 : \u2102).im| from hgt.le)\n rw [h\u03c1j] at h\n exact h\n rcases le_or_gt 0 (\u03c1 : \u2102).im with him | him\n \u00b7 apply Finset.mem_union_left\n rw [Set.Finite.mem_toFinset]\n refine \u27e8\u03c1.2, ?_, ?_\u27e9\n \u00b7 rw [abs_of_nonneg him] at hlo\n linarith\n \u00b7 rw [abs_of_nonneg him] at hup\n linarith\n \u00b7 apply Finset.mem_union_right\n rw [Set.Finite.mem_toFinset]\n refine \u27e8\u03c1.2, ?_, ?_\u27e9\n \u00b7 rw [abs_of_neg him] at hup\n linarith\n \u00b7 rw [abs_of_neg him] at hlo\n linarith\n have hsum_img : \u2211 \u03c1 \u2208 FS, (zeroMult (\u03c1 : \u2102) : \u211d)\n = \u2211 z \u2208 FS.image (Subtype.val), (zeroMult z : \u211d) := by\n rw [Finset.sum_image (fun x _ y _ h => Subtype.val_injective h)]\n have hdisj : Disjoint hW1.toFinset hW2.toFinset := by\n rw [Finset.disjoint_left]\n intro z hz1 hz2\n rw [Set.Finite.mem_toFinset] at hz1 hz2\n have h1 : (2 : \u211d) ^ j * X - 1 < z.im := hz1.2.1\n have h2 : z.im \u2264 -((2 : \u211d) ^ j * X) := hz2.2.2\n have hge : (1 : \u211d) \u2264 (2 : \u211d) ^ j * X := by\n have h1le : (1 : \u211d) \u2264 (2 : \u211d) ^ j := by exact_mod_cast Nat.one_le_two_pow\n nlinarith [h1le, hX]\n linarith\n calc \u2211 \u03c1 \u2208 FS, (zeroMult (\u03c1 : \u2102) : \u211d)\n = \u2211 z \u2208 FS.image (Subtype.val), (zeroMult z : \u211d) := hsum_img\n _ \u2264 \u2211 z \u2208 hW1.toFinset \u222a hW2.toFinset, (zeroMult z : \u211d) :=\n Finset.sum_le_sum_of_subset_of_nonneg himg (fun z _ _ => Nat.cast_nonneg _)\n _ = \u2211 z \u2208 hW1.toFinset, (zeroMult z : \u211d) + \u2211 z \u2208 hW2.toFinset, (zeroMult z : \u211d) :=\n Finset.sum_union hdisj\n _ = (Zeta23.Ncount ((2 : \u211d) ^ j * X - 1) ((2 : \u211d) ^ (j + 1) * X) : \u211d)\n + (Zeta23.Ncount (-(2 : \u211d) ^ (j + 1) * X) (-((2 : \u211d) ^ j * X)) : \u211d) := by\n rw [Zeta23.Ncount, Zeta23.Ncount, finsum_mem_eq_finite_toFinset_sum _ hW1,\n finsum_mem_eq_finite_toFinset_sum _ hW2, Nat.cast_sum, Nat.cast_sum]\n _ \u2264 A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n have h2jX1 : (1 : \u211d) \u2264 (2 : \u211d) ^ j * X := by\n have h1 : (1 : \u211d) \u2264 (2 : \u211d) ^ j := by exact_mod_cast Nat.one_le_two_pow\n nlinarith [h1, hX]\n have hpowX : (2 : \u211d) ^ (j + 1) * X = 2 * ((2 : \u211d) ^ j * X) := by\n rw [pow_succ']; ring\n have hlogpos : (0 : \u211d) \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_nonneg\n linarith [h2j1X]\n have h1 := Ncount_le_of_interval_gen (a := (2 : \u211d) ^ j * X - 1)\n (b := (2 : \u211d) ^ (j + 1) * X) (by linarith [hpowX, h2jX1])\n have h2 := Ncount_le_of_interval_gen (a := -(2 : \u211d) ^ (j + 1) * X)\n (b := -(2 : \u211d) ^ j * X) (by linarith [hpowX, h2jX1])\n -- the log arguments match L = log(3\u00b72^{j+1}X + 5)\n have hlog1 : Real.log (3 * max |(2 : \u211d) ^ j * X - 1| |(2 : \u211d) ^ (j + 1) * X| + 5)\n \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_le_log (by positivity)\n have hmax : max |(2 : \u211d) ^ j * X - 1| |(2 : \u211d) ^ (j + 1) * X|\n \u2264 (2 : \u211d) ^ (j + 1) * X := by\n apply max_le\n \u00b7 rw [abs_of_nonneg (by linarith [h2jX1])]\n nlinarith [h2jX, h2j1X]\n \u00b7 rw [abs_of_nonneg h2j1X.le]\n linarith [hmax]\n have hlog2 : Real.log (3 * max |-(2 : \u211d) ^ (j + 1) * X| |-(2 : \u211d) ^ j * X| + 5)\n \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_le_log (by positivity)\n have hmax : max |-(2 : \u211d) ^ (j + 1) * X| |-(2 : \u211d) ^ j * X|\n \u2264 (2 : \u211d) ^ (j + 1) * X := by\n apply max_le\n \u00b7 rw [abs_neg, abs_of_nonneg h2j1X.le]\n \u00b7 rw [abs_neg, abs_of_nonneg h2jX.le]\n nlinarith [h2jX, h2j1X]\n linarith [hmax]\n -- the lengths: b\u2212a+1 = 2^jX + 2 and 2^jX + 1\n have hlen1 : (2 : \u211d) ^ (j + 1) * X - ((2 : \u211d) ^ j * X - 1) + 1\n = (2 : \u211d) ^ j * X + 2 := by\n have hpow : (2 : \u211d) ^ (j + 1) = 2 * (2 : \u211d) ^ j := by rw [pow_succ']; ring\n rw [hpow]\n ring\n have hlen2 : -(2 : \u211d) ^ j * X - (-(2 : \u211d) ^ (j + 1) * X) + 1\n = (2 : \u211d) ^ j * X + 1 := by\n have hpow : (2 : \u211d) ^ (j + 1) = 2 * (2 : \u211d) ^ j := by rw [pow_succ']; ring\n rw [hpow]\n ring\n rw [hlen1] at h1\n rw [hlen2] at h2\n -- assemble: A\u2080(2^jX+2)L + A\u2080(2^jX+1)L = A\u2080(2^{j+1}X+3)L\n have hA0 := A0count_pos.le\n have h1' : (Zeta23.Ncount ((2 : \u211d) ^ j * X - 1) ((2 : \u211d) ^ (j + 1) * X) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ j * X + 2) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) :=\n h1.trans (mul_le_mul_of_nonneg_left hlog1 (by positivity))\n have h2' : (Zeta23.Ncount (-(2 : \u211d) ^ (j + 1) * X) (-((2 : \u211d) ^ j * X)) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ j * X + 1) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) :=\n h2.trans (mul_le_mul_of_nonneg_left hlog2 (by positivity))\n have hpow : (2 : \u211d) ^ (j + 1) * X = 2 * ((2 : \u211d) ^ j * X) := by rw [pow_succ']; ring\n linarith [h1', h2', hA0, hlogpos, hpow]\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 613,
"oldLines": 8,
"newStart": 613,
"newLines": 8,
"lines": [
" have hmax : max |-(2 : \u211d) ^ (j + 1) * X| |-(2 : \u211d) ^ j * X|",
" \u2264 (2 : \u211d) ^ (j + 1) * X := by",
" apply max_le",
"- \u00b7 rw [abs_neg, abs_of_nonneg h2j1X.le]",
"- \u00b7 rw [abs_neg, abs_of_nonneg h2jX.le]",
"+ \u00b7 rw [neg_mul, abs_neg, abs_of_nonneg h2j1X.le]",
"+ \u00b7 rw [neg_mul, abs_neg, abs_of_nonneg h2jX.le]",
" nlinarith [h2jX, h2j1X]",
" linarith [hmax]",
" -- the lengths: b\u2212a+1 = 2^jX + 2 and 2^jX + 1"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"Wait — the algebra at the end of iteratedDeriv_neg_zpow_neg_one_add is getting messy with the sign/exponent handling. Let me reconsider the target form.\n\nThe claim: iteratedDeriv k (fun s => −(s+c)^{−1}) s = −(−1)^k·k!·(s+c)^{−(k+1)}.\n\nThe step: the k+1 case: deriv of −(−1)^k·k!·(s+c)^{−(k+1)} = −(−1)^k·k!·(−(k+1))·(s+c)^{−(k+2)} — and the target: −(−1)^{k+1}·(k+1)!·(s+c)^{−(k+2)}. Check: −(−1)^k·(−(k+1)) = (−1)^k(k+1) = −(−1)^{k+1}(k+1) ✓ since −(−1)^{k+1} = (−1)^k ✓. So the goal: −(−1)^k·k!·((−(k+1):ℤ):ℂ)·(s+c)^{−(k+2)} = −(−1)^{k+1}·(k+1)!·(s+c)^{−(k+2)}.\n\nThe exponent forms: my statement uses `(-(k : ℤ) - 1)` for the k-th — so at k+1: `(-((k+1:ℕ):ℤ) - 1)` = −(k+1)−1 = −k−2 ✓ and the deriv's exponent: (−(k:ℤ)−1) − 1 = −k−2 ✓ same value, different expression — hexp bridges.\n\nMy ending block is convoluted. Let me simplify: after rw [h4] the goal is:\n −(−1)^k·↑(k!)·((−(k:ℤ)−1:ℤ):ℂ)·(s+c)^(−(k:ℤ)−1−1) = −(−1)^{k+1}·↑((k+1)!)·(s+c)^(−((k+1:ℕ):ℤ)−1)\nBoth exponents equal −k−2 (as ℤ): rewrite both to a canonical form via hexp on both sides... hmm — rw [hexp] only rewrites the LHS's exponent. Let me instead just: convert everything with push_cast and ring_nf — the exponents are INSIDE zpow atoms — ring_nf won't equate zpow atoms with different exponent EXPRESSIONS even if equal... — need the exponents syntactically equal first. Let me handle:\n```lean\n rw [h4]\n have hexp1 : (-(k : ℤ) - 1 - 1 : ℤ) = (-(k : ℤ) - 2 : ℤ) := by ring\n have hexp2 : (-((k + 1 : ℕ) : ℤ) - 1 : ℤ) = (-(k : ℤ) - 2 : ℤ) := by push_cast; ring\n rw [hexp1, hexp2]\n -- now: −(−1)^k·↑k!·((−(k:ℤ)−1:ℤ):ℂ)·X = −(−1)^{k+1}·↑((k+1)!)·X with X := (s+c)^(−(k:ℤ)−2)\n have hconst : ((-(k : ℤ) - 1 : ℤ) : ℂ) = -((k : ℂ) + 1) := by push_cast; ring\n rw [hconst, hfact] -- hfact : ((k+1)!:ℂ) = (k+1)·(k!:ℂ)\n rw [pow_succ] -- (−1)^{k+1} → (−1)^k·(−1)\n ring\n```\nAfter these: LHS: −(−1)^k·↑k!·(−(↑k+1))·X; RHS: −((−1)^k·(−1))·((↑k+1)·↑k!)·X — ring: LHS = (−1)^k·↑k!·(↑k+1)·X·(−1)·(−1)... let me just verify ring can: LHS = −A·B·(−(k+1))·X = A·B·(k+1)·X where A := (−1)^k, B := ↑k!. RHS = −(A·(−1))·((k+1)·B)·X = A·(k+1)·B·X ✓ equal by comm ✓ ring closes ✓.\n\nBut careful about hfact's rewrite direction and the RHS's factorial form: the goal's RHS has `↑((k+1)!)` — hmm — the statement's (k+1) case: `(k + 1) !` cast — `((k + 1) ! : ℂ)` — hfact : ((k+1)!:ℂ) = (↑k+1)·(↑k!... — hmm my hfact was ((k + 1 : ℕ) ! : ℂ) = (k + 1) * (k ! : ℂ) — via Nat.factorial_succ: (k+1)! = (k+1)·k! — push_cast... — hmm — Nat.factorial_succ : (n+1)! = (n+1) * n! ✓ then casts — let me write hfact as:\n```lean\n have hfact : (((k + 1) ! : ℕ) : ℂ) = ((k : ℂ) + 1) * (k ! : ℂ) := by\n rw [Nat.factorial_succ]\n push_cast\n ring -- ↑(k+1)·↑(k!) = (↑k+1)·↑k! — cast of (k+1) — push_cast ✓\n```\nHmm — Nat.factorial_succ : (k+1)! = (k+1) * k! — the cast: ↑((k+1)·k!) — push_cast → (↑(k+1))·↑(k!) → (↑k+1)·↑k! ✓ — and the target (↑k+1)·↑k! — ring ✓ — actually after push_cast it should be syntactic — `ring` safe.\n\nLet me rewrite the whole ending block of the zpow lemma cleanly. Replace from `have hfact` onward.","signature":""},{"type":"text","text":"The ending algebra of the zpow lemma is convoluted — rewriting it cleanly."},{"type":"tool_use","id":"Edit_397","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean","old_string":" rw [h4]\n -- algebra: the constants and the exponent\n have hfact : ((k + 1 : ℕ) ! : ℂ) = (k + 1) * (k ! : ℂ) := by\n rw [Nat.factorial_succ]\n push_cast\n ring\n have hexp : (-(k : ℤ) - 1 - 1 : ℤ) = (-((k + 1 : ℕ) : ℤ) - 1 : ℤ) := by\n push_cast\n ring\n have hsign : -((-1 : ℂ)) ^ (k + 1) = -((-1 : ℂ)) ^ k * -((-(k : ℤ) - 1 : ℤ) : ℂ) := by\n rw [pow_succ]\n push_cast\n ring\n rw [hexp, hfact]\n rw [hsign]\n ring_nf\n -- reconcile -(−1)^k·k!·((−(k+1))·X) with the two forms\n have h5 : (((-(k : ℤ) - 1 : ℤ) : ℂ)) = -((k : ℂ) + 1) := by push_cast; ring\n rw [h5]\n ring","new_string":" rw [h4]\n -- normalize the exponents to −(k:ℤ)−2, then the constants\n have hexp1 : (-(k : ℤ) - 1 - 1 : ℤ) = (-(k : ℤ) - 2 : ℤ) := by ring\n have hexp2 : (-((k + 1 : ℕ) : ℤ) - 1 : ℤ) = (-(k : ℤ) - 2 : ℤ) := by push_cast; ring\n rw [hexp1, hexp2]\n have hconst : ((-(k : ℤ) - 1 : ℤ) : ℂ) = -((k : ℂ) + 1) := by push_cast; ring\n have hfact : (((k + 1) ! : ℕ) : ℂ) = ((k : ℂ) + 1) * (k ! : ℂ) := by\n rw [Nat.factorial_succ]\n push_cast\n ring\n rw [hconst, hfact, pow_succ]\n ring"},"extra_content":null}]