[{"type":"thinking","thinking":"`Summable.tsum_finsetSum` exists (grep finds usages; the declaration must be named slightly differently in source or my grep for \"theorem Summable.tsum_finsetSum\" missed due to to_additive). It gives: ∑' over a FINSET-indexed family: `(Summable.tsum_finsetSum (h : ∀ i ∈ s, Summable (f i))) : ∑' i, ∑ x ∈ s, f i x = ∑ x ∈ s, ∑' i, f i x`-ish — it's the FINITE SUM OF TSUMS swap, not what I need.\n\nWhat I actually need: split a tsum over a subtype by a Finset of exceptions: ∑' i, f i = ∑ i ∈ s, f i + ∑' i, (if i ∈ s then 0 else f i)-style, or the complement-subtype tsum. The cleanest available: `tsum_eq_sum` for finsets? Hmm: `tsum_eq_sum (hf : ∀ i ∉ s, f i = 0) : ∑' i, f i = ∑ i ∈ s, f i`? That's for finite support. For the split: ∑' f = ∑' (f·indicator s) + ∑' (f·indicator sᶜ): via Summable.tsum_add of the two indicator-parts (each ≤ f pointwise for nonneg f ⟹ summable via of_norm_bounded hf.norm...) — then ∑' (f·indicator s) = ∑_{i ∈ s} f i via tsum_eq_sum (support ⊆ s) ✓. This is exactly the seriesTermSub pattern from 5e-iii (single_summable + tsum_eq_single) generalized to a finset — `tsum_eq_sum` for finsets: check name: `tsum_eq_sum (hf : ∀ b ∉ s, f b = 0)`? — I used tsum_eq_single in 5e-iii: `tsum_eq_single (a) (h : ∀ b ≠ a, f b = 0)`. For finsets: `tsum_eq_sum (hs : ∀ b ∉ s, f b = 0) : ∑' f = ∑ b ∈ s, f b`? Let me verify exists. Actually from memory: `tsum_eq_sum {s : Finset β} {f : β → α} (hf : ∀ b ∉ s, f b = 0) : ∑' b, f b = ∑ b in s, f b` — yes I'm fairly confident this exists (maybe as `tsum_eq_sum'`...). Let me check quickly then design the split lemma once:\n\n**Generic split helper** (prove once, reuse for each shell):\n```lean\nlemma tsum_split_finset {f : SubtypeZ → ℝ} (hf : Summable f) (s : Finset SubtypeZ) :\n    ∑' i, f i = ∑ i ∈ s, f i + ∑' i, (if i ∈ s then 0 else f i) := ...\n```\nvia: f = (if i ∈ s then f i else 0) + (if i ∈ s then 0 else f i) pointwise; both summable (of_norm_bounded hf.norm: ‖if...‖ ≤ ‖f i‖ ✓); Summable.tsum_add; and ∑' (if i ∈ s then f i else 0) = ∑_{i∈s} f i via tsum_eq_sum (support ⊆ s ✓).\n\nThen the bound: for the complement part ∑' (if i ∈ s then 0 else f i) ≤ ∑' (if i ∈ s then 0 else M i) with M summable: Summable.tsum_le_tsum (pointwise ≤, both summable) ✓.\n\nThe shells: s₀ := {‖ρ‖ ≤ 3}-finset; then the complement splits further by the SAME helper applied to the if-zeroed function (which is still summable) — chaining: complement of s₀ split by s₁ := {3 < ‖ρ‖ ≤ R/2}: ∑' (if ∉ s₀ then f else 0) = ∑_{s₁\\s₀}... — manageable but each split adds plumbing. With 6 shells that's 6 applications — each ~30 lines of plumbing = 180 lines just for splitting. Hmm.\n\nALTERNATIVE with much less plumbing: bound the whole norm-tsum by a SINGLE comparison with a majorant family defined by cases on the shell:\n\nFor each zero ρ, its term g ρ = m·R/(‖ρ‖·‖s−ρ‖) is bounded by a CASE-SPLIT majorant:\nM ρ := m·( case: ‖ρ‖ ≤ 3 → (1 + 1/‖ρ‖)·... hmm but then ∑' M over the subtype needs M summable — the critical-band majorant has 32Ĉ₀ factors and is bounded but the family must be summable over the zeros: M ρ := m·(min over the applicable bounds)... define M ρ := m·R/(‖ρ‖·D ρ) where D ρ := the applicable ‖s−ρ‖ lower bound — D ρ as a function of ρ (not shell-uniform)... \n\nThe comparison approach: ∑' g ≤ ∑' M requires M summable over the subtype. The shell-sum analysis IS the summability proof of M. No free lunch.\n\nOK — actually, let me simplify the shell structure to reduce the number of pieces. CLAIM: the following THREE-way split suffices:\n\nPiece LOW: {‖ρ‖ ≤ 3}: finite symbolic C_low := Σ (m·(1 + 1/‖ρ‖))-ish.\nPiece MID: {3 < ‖ρ‖ ≤ 2R}: here ‖s−ρ‖ ≥ |R − ‖ρ‖| AND... the term bound R/(‖ρ‖·|R−‖ρ‖)... the issue: zeros with ‖ρ‖ ≈ R (the critical annulus) — inside MID if I cut at 2R — the |R−‖ρ‖| can be 0! So MID must exclude the critical annulus [R−2, R+2]: MID := {3 < ‖ρ‖ ≤ 2R} ∖ (R−2, R+2)... messy. And the near-axis-arc alternative bound (|re|-split) for the critical band.\n\nHmm, alternatively: critical band handled with the FULL point-split: for s on the circle, EITHER |t| ≥ 10 (strip: γ-gap) or |t| < 10 (near-axis: re-split). Two versions of the critical-band term bound:\n- strip: ‖s−ρ‖ ≥ |t−γ| ≥ 1/(32Ĉ₀).\n- near-axis: ‖s−ρ‖ ≥ |re s − re ρ| ≥ √(R²−100) − 1 ≥ R/2.\nSo define the term bound for critical-band ρ: m·R/(‖ρ‖·g(s)) where g(s) := min over the two? — the bound used depends on s's arc — so the majorant family M depends on s's arc: fine — the lemma takes (hs : ‖s‖ = R) and splits on arcs INTERNALLY.\n\nOK — I think the pragmatic move is: write the big lemma with the 6-piece split via a sequence of `tsum_split_finset` applications. To reduce pain, prove the pieces as separate lemmas:\n\nB1. `seriesTail_lemma` (the |γ| > 2R tail as a tsum bound).\nB2. The finite-part bounds (low + mid shells + critical + upper band) as FINSET sum bounds.\nB3. The assembly: ‖seriesFun s‖ ≤ norm-tsum = finite parts + tail ≤ ...\n\nHmm — actually, WAIT. Let me reconsider whether the middle shells can ALL be folded into ONE crude bound that still gives o(R):\n\nFor 3 < ‖ρ‖ ≤ 2R (excluding critical): term ≤ R/(‖ρ‖·|R−‖ρ‖)... the problem was |R−‖ρ‖| small near R. What if I split at just TWO radii: {3 < ‖ρ‖ ≤ R−2} ∪ {R+2 ≤ ‖ρ‖ ≤ 2R}:\n- inner {3 < ‖ρ‖ ≤ R−2}: |R−‖ρ‖| ≥ 2: term ≤ R/(‖ρ‖·2) ≤ R/(2·3)·... no wait — term ≤ R/(‖ρ‖·(R−‖ρ‖)) and BOTH factors vary: the crudest uniform bound: R−‖ρ‖ ≥ 2 ⟹ term ≤ R/(2‖ρ‖) — and Σ_{3<‖ρ‖≤R−2} m/‖ρ‖ via dyadic ordinate shells = O(A₀(log R)²) as before — the dyadic shell sum is needed for THIS anyway.\n\nSo the dyadic machinery is needed for the inner part regardless. Let me just build a single dyadic-shell master lemma and apply it 4 times:\n\n**Master dyadic lemma**: for a function ψ(j)-bounded family... hmm. Actually the four applications have slightly different term bounds. Let me define them as four separate bounds each proved via the same window-count input (Ncount_le_of_interval_gen), with the dyadic index handled by `Finset.sum` over j ∈ range(⌈log₂ R⌉)... the dyadic sum over j is a FINSET sum over j : ℕ (j ≤ J) — and each j-shell is a finset of zeros — the shell-sum ≤ count·termbound — the counts via the interval lemma — and the total = Σ_{j} explicit ≤ integral/closed form...\n\nYou know, this is going to be long no matter what. Let me just start writing and get as far as the session allows, committing incrementally. Given the length already, let me write the 5e-v-b helpers file-section now: the split helper + the generalized interval count + the low-set definition + the master shell-bound lemma.\n\nActually — realistic scoping: the remaining work for 5e-v is likely 1000+ lines. The natural sub-stage break: this session already delivered 5e-v-a (committed). Let me continue with 5e-v-b helpers now and see how far we get; everything commits cleanly.\n\nLet me write the split helper + interval-generalization + low-set + tail bound now.","signature":""},{"type":"text","text":"The split machinery is clear. Writing 5e-v-b's helper layer now (tsum finset-split, generalized interval count, the low-zero constant, and the far-tail bound)."},{"type":"tool_use","id":"Bash_307","name":"Bash","input":{"command":"cd D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"theorem tsum_eq_sum\\b\\|lemma tsum_eq_sum\\b\" Mathlib/Topology/Algebra/InfiniteSum/ -r --include=*.lean | head -3 && grep -rn -A 3 \"theorem tsum_eq_sum\\b\" Mathlib/Topology/Algebra/InfiniteSum/Basic.lean 2>/dev/null | head -6","description":"tsum_eq_sum finset form"},"extra_content":null}]