[{"type":"thinking","thinking":"The additive version: `summable_of_hasFiniteSupport (h : HasFiniteSupport f) : Summable f` — but note the `[L.HasSupport]` constraint in the multipliable version... it's about summability to a value L? Hmm — actually `summable_of_hasFiniteSupport` requires the target to have a `HasSupport` instance? Looking at Weierstrass usage: `summable_of_hasFiniteSupport ((Set.finite_singleton l₀).subset (by simp))` — takes a Set.Finite proof of support-containment. `HasFiniteSupport f` is a structure: `(Set.finite (Function.support f))`-wrapper? `Function.HasFiniteSupport f := (Function.support f).Finite`. The lemma signature: `summable_of_hasFiniteSupport (h : HasFiniteSupport f) : Summable f` probably (with the [L.HasSupport] for the L-valued version — the deprecated alias suggests the plain version exists). \n\nSimpler alternative — avoid finite-support entirely: use `Summable.of_norm_bounded` with the dominator D' = fam + (finite-support modification)... The cleanest alternative: `Summable.of_norm_bounded` where D covers ALL points with the if-then-else; prove `Summable D` via: D = fam + E with E finite support — still needs finite-support summability. Alternative standard trick: `summable_of_norm_bounded'`... \n\nActually simplest: avoid the issue by making the dominator the SUM of the always-valid bound: for points with ‖ρ‖ < 2n, bound ‖liSummand n ρ‖ by a CONSTANT C(n) valid on the whole subtype (if such exists — does ‖liSummand‖ have a uniform bound on ALL zeros? ‖liSummand n ρ‖ = mult·|Re f(ρ)| and |Re f| ≤ |f| ≤ 1 + |1−1/ρ|ⁿ: for small ρ (e.g. ρ → 0?) — no: nontrivial zeros have |ρ| ≥ ... hmm, zeros with tiny |ρ|? The strip zeros: the smallest |γ| is 14.134 — but proving a lower bound on the first zero in Lean requires the numerical zero-free result (not available). HOWEVER: ρ.re ∈ (0,1) and ρ.im = γ with NO lower bound available... wait — actually is there a cheap bound? |1−1/ρ| with ρ = σ+iγ: |1/ρ| = 1/|ρ|: for γ → 0 with σ ∈ (0,1): |ρ| could be small ONLY IF there were zeros near the real axis — those don't exist (ζ(x) < 0 for x ∈ (0,1) real — the eta argument) — but PROVING that is work. However — we don't need a uniform bound on ALL zeros: the dominator on the finite ball can use per-point values ‖liSummand n ρ‖ (that's what the if-then-else does) — the finite-support issue is intrinsic. So use summable_of_hasFiniteSupport with the finite ball set. `Function.HasFiniteSupport f` — the structure: `def Function.HasFiniteSupport (f : α → β) : Prop := (Function.support f).Finite`? And `summable_of_hasFiniteSupport` — from the deprecated alias line: `summable_of_finite_support := summable_of_hasFiniteSupport` ✓ so `summable_of_hasFiniteSupport` exists and takes the finite-support proof. The Weierstrass usage `summable_of_hasFiniteSupport ((Set.finite_singleton l₀).subset (by simp))` — takes `Set.Finite.subset` proof — so the argument is `(h : (Function.support f).Finite)` or a HasFiniteSupport wrapper — `.subset` produces Set.Finite — so the argument is a Set.Finite proof of something. Good enough: I'll construct `Function.HasFiniteSupport E` via its definition `(Function.support E).Finite`.\n\nLet me check HasFiniteSupport def quickly... I'll just write `(Function.support E).Finite` and use it — if the lemma wants the wrapper, it's defeq.\n\nAlso `Set.Finite.of_finite_image` ✓ exists.\n\nNow write the final block. Also remember the deprecated alias note: the non-deprecated name is `summable_of_hasFiniteSupport`.\n\nOne more consideration for `hbase`: `(WeilEF.zero_sum_inv_sq zetaSeam).mul_left ((9/2)*(n:ℝ)^2)` — `.mul_left` on Summable: `Summable.mul_left (a : α) (hf : Summable f) : Summable (fun i => a * f i)` — signature order: `Summable.mul_left (a) (hf)` or `hf.mul_left a`? As dot notation `hf.mul_left a` ✓ standard.\n\nAnd the hbase family form: (9/2)n² * (mult/(1+normSq)) — matches D's if-branch `(9/2)*n^2*(zeroMult ρ : ℝ)/(1+normSq...)` — I wrote D's branch as `(9 / 2) * n ^ 2 * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))` — elaborates as ((9/2)*n²*mult)/(1+normSq) vs hbase's (9/2)n²*(mult/(1+normSq)) — equal by ring (div_eq_mul_inv, mul assoc). In the funext for D = fam + E I'll handle with field_simp/ring.\n\nLet me now write the whole final block and append to Scratch.lean.","signature":""},{"type":"text","text":"All API names confirmed. Appending the summability assembly to Scratch."},{"type":"tool_use","id":"Bash_140","name":"Bash","input":{"command":"cat >> /d/Python/Quantum/research/lean/NguyenRH1/Scratch.lean << 'EOF'\n\n/-! ### The comparison 1 + ‖γ_ρ‖² ≤ (9/4)‖ρ‖² and the dominator -/\n\n/-- For re z ∈ [0,1] and 2n ≤ ‖z‖ (n ≥ 1): 1 + ‖γ_z‖² ≤ (9/4)·‖z‖². -/\nlemma normSq_gammaOf_le_mul_norm_sq {n : ℕ} (hn : 1 ≤ n) {z : ℂ}\n    (hzre0 : 0 ≤ z.re) (hzre1 : z.re ≤ 1) (hz : 2 * n ≤ ‖z‖) :\n    1 + Complex.normSq (gammaOf z) ≤ 9 / 4 * ‖z‖ ^ 2 := by\n  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn\n  have hz2 : ‖z‖ ^ 2 = z.re ^ 2 + z.im ^ 2 := by\n    rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n    ring\n  have hz4 : 4 * n ^ 2 ≤ ‖z‖ ^ 2 := by\n    have h := pow_le_pow_left₀ (by positivity : (0:ℝ) ≤ 2 * n) hz 2\n    nlinarith [h]\n  have hre2 : z.re ^ 2 ≤ 1 := by nlinarith [hzre0, hzre1]\n  have him : 1 ≤ z.im ^ 2 := by nlinarith [hz2, hz4, hre2]\n  have hgam : Complex.normSq (gammaOf z) = z.im ^ 2 + (1 / 2 - z.re) ^ 2 := by\n    rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]\n    ring\n  rw [hgam, hz2]\n  nlinarith [hzre0, hzre1, him, sq_nonneg (1 / 2 - z.re), sq_nonneg z.re]\n\n/-- Norm of the paired summand: mult·|Re f(ρ)|. -/\nlemma liSummand_norm (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    ‖liSummand n ρ‖ = (zeroMult ρ : ℝ) * |(1 - (1 - 1 / (ρ : ℂ)) ^ n).re| := by\n  rw [liSummand_eq n ρ, norm_mul, RCLike.norm_natCast, RCLike.norm_ofReal]\n\n/-- The main bound: for 2n ≤ ‖ρ‖, ‖liSummand n ρ‖ ≤ (9/2)n²·mult/(1+‖γ_ρ‖²). -/\nlemma liSummand_norm_le {n : ℕ} (hn : 1 ≤ n) (ρ : {ρ : ℂ // IsNontrivialZero ρ})\n    (hρ : (2 : ℝ) * n ≤ ‖(ρ : ℂ)‖) :\n    ‖liSummand n ρ‖ ≤\n      (9 / 2) * n ^ 2 * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by\n  have hz := ρ.2\n  have hre0 : 0 ≤ (ρ : ℂ).re := hz.2.1.le\n  have hre1 : (ρ : ℂ).re ≤ 1 := hz.2.2.le\n  have hcore := re_li_summand_le hn hre0 hre1 hρ\n  have hcomp := normSq_gammaOf_le_mul_norm_sq hn hre0 hre1 hρ\n  have hnpos : (0 : ℝ) < n := by exact_mod_cast hn\n  have hz0 : (0 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_lt_of_le (by positivity) hρ\n  have hg0 : (0 : ℝ) < 1 + Complex.normSq (gammaOf (ρ : ℂ)) := by\n    have h := Complex.normSq_nonneg (gammaOf (ρ : ℂ))\n    linarith\n  have key : (zeroMult ρ : ℝ) * (2 * n ^ 2 / ‖(ρ : ℂ)‖ ^ 2)\n      ≤ (9 / 2) * n ^ 2 * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by\n    rw [le_div_iff₀ hg0]\n    have hbound : (zeroMult ρ : ℝ) * (2 * n ^ 2 / ‖(ρ : ℂ)‖ ^ 2) *\n          (1 + Complex.normSq (gammaOf (ρ : ℂ)))\n        ≤ (zeroMult ρ : ℝ) * (2 * n ^ 2 / ‖(ρ : ℂ)‖ ^ 2) * ((9 / 4) * ‖(ρ : ℂ)‖ ^ 2) :=\n      mul_le_mul_of_nonneg_left hcomp (by positivity)\n    exact hbound.trans (by field_simp; ring)\n  rw [liSummand_norm]\n  exact (mul_le_mul_of_nonneg_left hcore (Nat.cast_nonneg _)).trans key\n\n/-- The paired Li summand is absolutely summable over the nontrivial zeros.\nUses Zeta23's `WeilEF.zero_sum_inv_sq` (Σ mult/(1+‖γ_ρ‖²) < ∞, proved) via\nthe tail bound of `liSummand_norm_le`; the ball {‖ρ‖ < 2n} contributes a\nfinite set (Mathlib `IsCompact.inter_riemannZetaZeros_finite`). -/\ntheorem liSummable (n : ℕ) : Summable (liSummand n) := by\n  rcases Nat.eq_zero_or_pos n with h0 | hn\n  · subst h0\n    have h : liSummand 0 = fun _ => (0 : ℂ) := by\n      funext ρ\n      simp [liSummand]\n    rw [h]\n    exact summable_zero\n  · -- the base summable family (Zeta23, proved)\n    have hbase : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n        (9 / 2) * (n : ℝ) ^ 2 * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))) := by\n      have h := (WeilEF.zero_sum_inv_sq zetaSeam).mul_left ((9 / 2) * (n : ℝ) ^ 2)\n      exact h\n    -- the dominator\n    set D : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>\n      if (2 : ℝ) * n ≤ ‖(ρ : ℂ)‖ then\n        (9 / 2) * n ^ 2 * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))\n      else ‖liSummand n ρ‖ with hDdef\n    -- the correction E = D − base has finite support\n    have hfin : {ρ : {ρ // IsNontrivialZero ρ} | ¬ ((2 : ℝ) * n ≤ ‖(ρ : ℂ)‖)}.Finite := by\n      have hcomp : IsCompact (Metric.closedBall (0 : ℂ) (2 * n)) :=\n        isCompact_closedBall _ _\n      have hzeros : (Metric.closedBall (0 : ℂ) (2 * n)) ∩ {ρ : ℂ | IsNontrivialZero ρ}\n          ⊆ (Metric.closedBall (0 : ℂ) (2 * n)) ∩ riemannZetaZeros := by\n        intro z hz\n        exact ⟨hz.1, hz.2.1⟩\n      have hfin2 := (hcomp.inter_riemannZetaZeros_finite).subset hzeros\n      have himg : (Subtype.val '' {ρ : {ρ // IsNontrivialZero ρ} |\n          ¬ ((2 : ℝ) * n ≤ ‖(ρ : ℂ)‖)}).Finite := by\n        apply hfin2.subset\n        rintro z ⟨ρ, hρ, rfl⟩\n        refine ⟨?_, ρ.2⟩\n        simp only [Metric.mem_closedBall, dist_zero_right]\n        exact le_of_lt (lt_of_not_ge hρ)\n      exact Set.Finite.of_finite_image himg (Subtype.val_injective.injOn)\n    have hE : Summable (fun ρ : {ρ // IsNontrivialZero ρ} =>\n        D ρ - (9 / 2) * (n : ℝ) ^ 2 * ((zeroMult ρ : ℝ) /\n          (1 + Complex.normSq (gammaOf ρ)))) := by\n      apply summable_of_hasFiniteSupport\n      apply hfin.subset\n      intro ρ hρ\n      simp only [Function.mem_support, ne_eq] at hρ\n      by_contra hball\n      apply hρ\n      have hball' : (2 : ℝ) * n ≤ ‖(ρ : ℂ)‖ := not_not.mp hball\n      simp only [D, if_pos hball', sub_self]\n    have hD : Summable D := by\n      have hsum := hbase.add hE\n      have heq : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n          (9 / 2) * (n : ℝ) ^ 2 * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))) +\n            (D ρ - (9 / 2) * (n : ℝ) ^ 2 * ((zeroMult ρ : ℝ) /\n              (1 + Complex.normSq (gammaOf ρ))))) = D := by\n        funext ρ\n        ring\n      rw [heq] at hsum\n      exact hsum\n    refine Summable.of_norm_bounded hD (fun ρ => ?_)\n    by_cases hρ : (2 : ℝ) * n ≤ ‖(ρ : ℂ)‖\n    · simp only [D, if_pos hρ]\n      exact liSummand_norm_le hn ρ hρ\n    · simp only [D, if_neg hρ, le_refl]\nEOF\ncd /d/Python/Quantum/research/lean/NguyenRH1 && export PATH=\"$HOME/.elan/bin:$PATH\" && lake env lean Scratch.lean 2>&1 | head -40","description":"Append summability assembly and check","timeout":420000},"extra_content":null}]