[{"type":"thinking","thinking":"`norm_term_eq`: ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / n ^ s.re — perfect for the comparison lemma. For the Λ terms at 3 vs 2:\n\n‖term Λ 3 n‖ = (n = 0 ? 0 : Λ(n)/n³) and ‖term Λ 2 n‖ = (n = 0 ? 0 : Λ(n)/n²). For n ≠ 0: Λ(n)/n³ = (1/n)·(Λ(n)/n²) ≤ (1/2)·(Λ(n)/n²) when 2 ≤ n (1/n ≤ 1/2 ✓); n = 1: Λ(1) = 0 → both 0 ✓ (Λ(1) = 0 — vonMangoldt at 1: `ArithmeticFunction.vonMangoldt_one` = 0 ✓ exists presumably).\n\nThe comparison lemma:\n```lean\nlemma norm_term_vonMangoldt_three_le_half (n : ℕ) :\n    ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖ ≤\n      (1 / 2) * ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖ := by\n  rw [norm_term_eq, norm_term_eq]\n  split\n  · norm_num\n  · next hn =>\n    -- goal: Λ(n)/n³ ≤ (1/2)·(Λ(n)/n²)\n    have hn2 : 2 ≤ n := Nat.two_le_iff_ne_zero_and_one_lt... \n```\nHmm — n ≠ 0 means n ≥ 1; for n = 1, Λ(1) = 0 → both sides 0. For n ≥ 2: the ratio. So handle n = 1 specially:\n```\n  · next hn =>\n    rcases eq_or_ne n 1 with rfl | hn1\n    · simp [ArithmeticFunction.vonMangoldt_one]  -- Λ(1) = 0: both sides 0\n    · have hn2 : 2 ≤ n := by omega  -- n ≠ 0 ∧ n ≠ 1 ⟹ 2 ≤ n\n      -- Λ(n)/n³ ≤ (1/2)·Λ(n)/n²\n      have hΛnn : (0:ℝ) ≤ (ArithmeticFunction.vonMangoldt n : ℝ) := ArithmeticFunction.vonMangoldt_nonneg\n      have e : (ArithmeticFunction.vonMangoldt n : ℝ) / (n:ℝ) ^ 3 =\n          (1 / (n:ℝ)) * ((ArithmeticFunction.vonMangoldt n : ℝ) / (n:ℝ) ^ 2) := by\n        field_simp [show (n:ℝ) ≠ 0 by positivity]\n        ring\n      rw [e]\n      have h12 : (1 : ℝ) / (n:ℝ) ≤ 1 / 2 := by\n        rw [div_le_div_iff_of_pos_left (by norm_num : (0:ℝ) < 1) (by positivity : (0:ℝ) < 2) (by positivity : (0:ℝ) < n)]\n        exact_mod_cast hn2\n      calc (1 / (n:ℝ)) * ((ArithmeticFunction.vonMangoldt n : ℝ) / (n:ℝ) ^ 2)\n          ≤ (1 / 2) * ((ArithmeticFunction.vonMangoldt n : ℝ) / (n:ℝ) ^ 2) := by\n            apply mul_le_mul_of_nonneg_right _ (by positivity)\n            exact h12\n        _ = (1 / 2) * ‖...‖ := by rw [norm_term_eq, if_neg hn]\n```\nHmm — the norm_term_eq's if: the goal after `rw [norm_term_eq, norm_term_eq]; split` — the two ifs share the condition n = 0: `split` handles the if on the GOAL (both ifs split together? `split` splits the FIRST if; with two ifs with the same condition it might handle both or need twice). The norm_term_le_of_re_le_re proof above did exactly `simp only [norm_term_eq]; split; · rfl; · next hn => gcongr; ...` — so split handles both ifs in one go (they reduce on the same condition) ✓ clone that pattern.\n\nAlso — wait, the norm of the Λ value: ‖(ArithmeticFunction.vonMangoldt n : ℂ)‖ = Λ(n) (real, nonneg): the norm_term_eq gives ‖f n‖/n^s.re with f n = (Λ n : ℂ): ‖(Λ n : ℂ)‖ = Λ n as a real (Complex.norm_of_nonneg vonMangoldt_nonneg / or the norm is just the real value: (‖(Λ n : ℂ)‖ : ℝ) = Λ n — need `Complex.norm_ofReal`/`norm_of_nonneg`... In the goal after norm_term_eq, the LHS is ‖(Λ n : ℂ)‖ / n^3 — the `e` computation needs ‖(Λ n:ℂ)‖ = Λ n (as reals): `have hΛ : ‖(ArithmeticFunction.vonMangoldt n : ℂ)‖ = ArithmeticFunction.vonMangoldt n := by rw [Complex.norm_eq_abs, ← Real.norm_eq_abs, Real.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg]` — or `norm_of_nonneg vonMangoldt_nonneg` directly (Complex.norm_of_nonneg exists? `Complex.norm_of_nonneg (hx : 0 ≤ x) : ‖(x : ℂ)‖ = x` ✓ exists).\n\nOK — and the summability for the tsum comparison:\n```\nlemma dirichletC3_le_half : (∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖) ≤ 1 / 2 := by\n  have hsum3 : Summable (fun n : ℕ => ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsum2 : Summable ... := (same at 2)\n  calc ∑' n, ‖term Λ 3 n‖\n      ≤ ∑' n, (1/2) * ‖term Λ 2 n‖ := Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_three_le_half n) hsum3 (hsum2.mul_left _)\n    _ = (1/2) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n    _ ≤ 1 / 2 := by linarith [dirichletC2_le_one]\n```\n`Summable.tsum_le_tsum (h : ∀ n, f n ≤ g n) (hf : Summable f) (hg : Summable g) : ∑' f ≤ ∑' g` ✓ (used in the C2 proof ✓).\n\nAnd the zeta bound:\n```\n/-- ‖ζ′/ζ s‖ ≤ 1/2 for re s ≥ 3 (the C = 0.5 dog-leg constant: the\ntermwise 3-vs-2 comparison + dirichletC2 ≤ 1). -/\nlemma norm_logDeriv_zeta_le_half {s : ℂ} (hs : 3 ≤ s.re) :\n    ‖logDeriv riemannZeta s‖ ≤ 1 / 2 := by\n  have hs2 : 2 ≤ s.re := by linarith\n  have hle := norm_logDeriv_zeta_le_dirichlet hs2\n  -- hmm — that gives ≤ dirichletC2, not the sharper 3-bound...\n```\nWAIT — norm_logDeriv_zeta_le_dirichlet bounds by dirichletC2 (the s=2 tsum). For the sharper s=3 comparison I need the s=3 tsum: ‖LSeries Λ s‖ ≤ ∑'‖term Λ s‖ ≤ ∑'‖term Λ 3‖ (re 3 ≤ re s) — then dirichletC3 ≤ 1/2. So I need the full C3-shaped clone:\n\n```\nlemma norm_logDeriv_zeta_le_dirichletC3 {s : ℂ} (hs : 3 ≤ s.re) :\n    ‖logDeriv riemannZeta s‖ ≤ ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖ :=\n  -- clone of norm_logDeriv_zeta_le_dirichlet with 3 in place of 2\n\nlemma norm_logDeriv_zeta_le_half {s : ℂ} (hs : 3 ≤ s.re) :\n    ‖logDeriv riemannZeta s‖ ≤ 1 / 2 :=\n  le_trans (norm_logDeriv_zeta_le_dirichletC3 hs) dirichletC3_le_half\n```\n\nFor uniformity with dirichletC2, define dirichletC3:\n```\ndef dirichletC3 : ℝ := ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖\n```\nthen dirichletC3_le_half : dirichletC3 ≤ 1/2 and the clone bounds by dirichletC3.\n\nThen the V_left assembly:\n```\n/-- The left-lift bound (D-074 §3.3 V_left): for T² ≥ n and 0 < T ≤ U,\n‖VIntegral (Jlag n) 3 T U‖ ≤ (U − T)·(e^{5/2}+1)/2. The zeta factor\n‖ζ′/ζ(3+it)‖ ≤ 1/2 (dirichletC3 ≤ 1/2); the kernel ≤ e^{5/2}+1. -/\ntheorem vIntegral_Jlag_three_norm_le {n : ℕ} {T U : ℝ}\n    (hT0 : (0 : ℝ) < T) (hTU : T ≤ U) (hTn : (n : ℝ) ≤ T ^ 2) :\n    ‖VIntegral (Jlag n) 3 T U‖ ≤ (U - T) * (Real.exp (5 / 2) + 1) / 2 := by\n  unfold VIntegral\n  rw [norm_smul, Complex.norm_I, one_mul]\n  -- ‖∫_T^U Jlag (3 + t·I) dt‖ ≤ ∫_T^U ‖Jlag‖ ≤ (U−T)·sup\n  have hcont : ContinuousOn (fun t : ℝ => Jlag n ((3 : ℝ) + t * Complex.I)) (Set.Icc T U) := by\n    intro t ht\n    exact (Jlag_differentiableAt_dogleg (by simp : 3 ≤ ((3:ℝ) + t*I).re) (by\n      simp [ht.1, hT0] : 0 < ((3:ℝ) + t*I).im)).continuousAt.continuousWithinAt\n  have hbound : ∀ t ∈ Set.Icc T U, ‖Jlag n ((3 : ℝ) + t * Complex.I)‖ ≤ (Real.exp (5/2) + 1) * (1/2) := by\n    intro t ht\n    have ht2 : (n : ℝ) ≤ t ^ 2 := by\n      -- t ≥ T ⟹ t² ≥ T² ≥ n ✓ (t ≥ T > 0)\n      have htT : T ≤ t := ht.1\n      nlinarith [hTn, hT0]\n    have h1 := kFun_three_add_it_norm_le_exp_five_halves_add_one ht2\n    have h2 := norm_logDeriv_zeta_le_half (s := (3:ℝ) + t * Complex.I) (by simp)\n    unfold Jlag\n    rw [show Jlag n ((3:ℝ) + t * Complex.I) = kFun n ((3:ℝ) + t * Complex.I) *\n        (logDeriv riemannZeta ((3:ℝ) + t * Complex.I)) from rfl]\n```\nHmm — Jlag n s = kFun n s * (-(deriv ζ s/ζ s)) and logDeriv ζ s = deriv ζ s/ζ s (logDeriv def: logDeriv f = f'/f ✓ so −(deriv/ζ) = −logDeriv). ‖−logDeriv‖ = ‖logDeriv‖ ✓.\n\n```\n    calc ‖kFun n _ * (-(deriv ζ _ / ζ _))‖\n        ≤ ‖kFun n _‖ * ‖logDeriv ζ _‖ := by rw [norm_mul, ← norm_neg]; rfl?? \n```\nlogDeriv f s = deriv f s / f s (Mathlib: logDeriv f = fun x => deriv f x / f x — the Pi.div form). So −(deriv ζ s/ζ s) = −logDeriv ζ s. ‖−logDeriv‖ = ‖logDeriv‖. The norm_logDeriv_zeta_le_half is stated on ‖logDeriv riemannZeta s‖ ✓. So:\n\n```\n    have hJ : Jlag n ((3:ℝ) + t * Complex.I) = kFun n ((3:ℝ) + t * Complex.I) *\n        (-logDeriv riemannZeta ((3:ℝ) + t * Complex.I)) := rfl\n    calc ‖Jlag n _‖ = ‖kFun n _‖ * ‖logDeriv ζ _‖ := by rw [hJ, norm_mul, norm_neg]\n      _ ≤ (Real.exp (5/2) + 1) * (1/2) := by\n          apply mul_le_mul h1 h2 (norm_nonneg _) (by positivity)\n```\nmul_le_mul (h1 : a ≤ b) (h2 : c ≤ d) (hc : 0 ≤ c) (hb : 0 ≤ b) : a*c ≤ b*d ✓ — hc : 0 ≤ ‖logDeriv‖ ✓ (norm_nonneg); hb : 0 ≤ e^{5/2}+1 ✓ positivity.\n\nThen the integral bound:\n```\n  calc ‖∫ t in T..U, Jlag n ((3:ℝ) + t * Complex.I)‖\n      ≤ (U - T) * ((Real.exp (5/2) + 1) * (1/2)) := by\n        apply intervalIntegral.norm_integral_le_of_norm_le_const hTU hbound\n      _ = (U - T) * (Real.exp (5 / 2) + 1) / 2 := by ring\n```\n`intervalIntegral.norm_integral_le_of_norm_le_const (hab : a ≤ b) (hf : ∀ x ∈ Set.Icc a b, ‖f x‖ ≤ C) : ‖∫ x in a..b, f x‖ ≤ C * (b - a)` — check the exact name/form: Mathlib has intervalIntegral.norm_integral_le_of_norm_le_const (hab : a ≤ b) (h : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C) : ‖∫ x in a..b, f x‖ ≤ C * |b - a|?? — there are variants. Let me check quickly. There's also `intervalIntegral.norm_integral_le_of_norm_le_const'`. I'll grep.\n\nAlso the norm_smul on I • x: ‖(I : ℂ) • x‖ = ‖I‖·‖x‖: norm_smul gives ‖I‖ * ‖x‖; Complex.norm_I : ‖Complex.I‖ = 1 ✓. Hmm — VIntegral f x y₁ y₂ = I • (∫ ...) with • being ℂ-scalar on ℂ — norm_smul : ‖c • x‖ = ‖c‖ * ‖x‖ ✓.\n\nAlso the interval integral ∫ t in T..U: VIntegral's def uses `∫ y in y₁..y₂, f (x + y * I)` — the intervalIntegral with the intervalIntegral Integrable condition?? The norm bound lemma needs integrability: norm_integral_le_of_norm_le_const might not require it (the junk-value convention) — the version without integrability: `intervalIntegral.norm_integral_le_of_norm_le_const'`? Hmm — safest: provide integrability (ContinuousOn ✓ gives IntervalIntegrable via ContinuousOn.intervalIntegrable).\n\nLet me check the exact lemma names in this Mathlib for the norm-of-interval-integral bound.","signature":""},{"type":"text","text":"Checking the exact interval-integral norm bound lemma names."},{"type":"tool_use","id":"Bash_202","name":"Bash","input":{"command":"cd D:/Python/Quantum/zeta-23-lean && grep -rn \"norm_integral_le_of_norm_le_const\\|norm_intervalIntegral_le\" .lake/packages/mathlib/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean 2>/dev/null | head -8; grep -rn \"theorem.*norm_integral_le_of_norm_le_const\" .lake/packages/mathlib/Mathlib/ -r 2>/dev/null | head -5","description":"Find interval-integral norm bound lemmas"},"extra_content":null}]