[{"type":"thinking","thinking":"Now §3: the parameter-integral hasDerivAt for the B₂ integral on re s > −1. Clone of Zeta23's hasDerivAt_Zeta0Integral with the extra decay. Let me adapt their proof:\n\n```lean\n/-- The B̃₂ parameter integral is differentiable on re s > −1. -/\ntheorem hasDerivAt_b2Integral {s : ℂ} (hs : -1 < s.re) :\n    HasDerivAt (fun z : ℂ => ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-z - 2))\n      (∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) * (-Real.log x))) s := by\n  set f : ℝ → ℂ := fun x ↦ (b2Fun x : ℂ)\n  set F : ℂ → ℝ → ℂ := fun z x ↦ (x : ℂ) ^ (-z - 2) * f x\n  set F' : ℂ → ℝ → ℂ := fun z x ↦ (x : ℂ) ^ (-z - 2) * (-Real.log x) * f x\n  set ε := (s.re + 1) / 2\n  have ε_pos : 0 < ε := by positivity? — (s.re+1)/2 > 0 from hs ✓ by linarith\n  set bound : ℝ → ℝ := fun x ↦ |x ^ (-(s.re + 3)/2)| * |Real.log x|  -- hmm: need |x^(−z−2)| ≤ bound-ish: for z ∈ ball(s, ε): re(−z−2) ≤ ... |x^(−z−2)| = x^(−re z−2) ≤ x^(−(σ−ε)−2) with −(σ−ε)−2 = −σ−2+ε = −σ−2+(σ+1)/2 = (−σ−3)/2 — hmm: −σ − 2 + (σ+1)/2 = (−2σ − 4 + σ + 1)/2 = (−σ−3)/2: for σ > −1: (−σ−3)/2 < −1 ✓ integrable. So bound x = x^((−σ−3)/2)·|log x| + the |f| ≤ 1/8 factor and the F' form — the Zeta23 bound was |x^(−s.re/2−1)|·|log x| and they absorbed |f| ≤ 1/2 via ≤ 1·|...| hmm — they had bound := |x ^ (-s.re/2 - 1)| * |log x| and in h_bound1: ‖F' z x‖ = |x^(−z.re−1)|·|log x|·|f x| ≤ |x^(−z.re−1)|·|log x|·(1/2)... and then ≤ bound with the 1/2 ≤ 1. I'll do the same with 1/8 ≤ 1.\n  ...\n  have bound_integrable : Integrable bound (volume.restrict (Ioi 1)) := integrable_log_over_pow (r := -(s.re + 1)/2) (by linarith) (by norm_num)\n```\nTheir integrable_log_over_pow {r} (rneg : r < 0) {N} (Npos : 0 < N) : IntegrableOn (fun x => ‖x^(r−1)‖·‖log x‖) (Ioi N): with r−1 = (−σ−3)/2 ⟹ r = (−σ−1)/2 < 0 ✓ (σ > −1). ✓.\n\nThe hasDerivAt piece: `HasDerivAt.comp (h' := ...) (fun w ↦ x ^ w)` — their proof used `HasDerivAt.const_cpow (c := (x:ℂ)) (f := fun w ↦ w) (f' := 1) (x := -z-1) (hasDerivAt_id _) ?_` — const_cpow : HasDerivAt (fun w => c ^ (f w)) (c^(f z) * log c * f')?? — they used it with the side condition about log — for x ≥ 1 > 0: log x real... `HasDerivAt.const_cpow (hf : HasDerivAt ℂ f f' z) (hc : c ≠ 0 ∨ ...)`: I'll mirror their exact usage:\n```\n    convert! HasDerivAt.comp (h := fun w ↦ -w-2) (h' := -1) (h₂ := fun w ↦ x ^ w)\n      (h₂' := x ^ (-z-2) * Real.log x) (x := z) ?_ ?_ using 0\n    · simp only [mul_neg, mul_one]; congr! 2\n    · convert! HasDerivAt.const_cpow (c := (x : ℂ)) (f := fun w ↦ w) (f' := 1) (x := -z-2)\n        (hasDerivAt_id _) ?_ using 1\n      · simp only [mul_one, mul_eq_mul_left_iff, cpow_eq_zero_iff, ofReal_eq_zero, ne_eq]\n        left\n        rw [Complex.ofReal_log]\n        linarith\n      · right\n        intro h\n        ... (the −z−2 = 0 exclusion via the ball)\n    · apply hasDerivAt_id _ |>.neg |>.sub_const\n```\nHmm their h₂ exponent was −w−1 (their F used ^(−z−1)); mine −w−2. The side conditions of const_cpow: `HasDerivAt.const_cpow (hf : HasDerivAt ℂ f f' x) (h : f x ≠ 0 ∨ c ≠ 0)?`? Their discharge: `cpow_eq_zero_iff` + ofReal_log: the first bullet proved... `(x:ℂ)^(−z−1) * log x` form matching: mul_eq_mul_left_iff: either log-cpow equality or the base zero... Their first `·` goal after convert! was something like `x ^ (-z-1) * Real.log x * 1 = ...`. Honestly — I'll clone their proof structure with −1 → −2 exponent changes and iterate on errors. The key differences: ε := (s.re + 1)/2 (their ε := s.re/2), bound exponent (−s.re−3)/2 vs their (−s.re/2−1), f := ↑b2Fun (continuous ⟹ their measurability easier: they used Measurable.comp Int.measurable_floor for B̃₁; b2Fun is continuous ✓ simpler).\n\nTheir ball-membership side-goal pattern (the `right` bullet): excluded −z−1 = 0 via the ball: z ∈ ball(s, ε), if −z−1 = 0: z = −1: dist s (−1) ≥ ... for mine: if −z−2 = 0: z = −2: dist(s, −2) < ε = (σ+1)/2: but dist(s, −2) ≥ |re s − (−2)| = σ+2 > σ+1 > ε contradiction ✓ adapt.\n\nAlso their `IoiSubIoi1` was about Ioi N ⊆ {1 < x} — for N = 1: Ioi 1 ⊆ {1 < x} ✓ trivially.\n\nActually — their h_bound1 works on {x | 1 < x} — for N = 1 same. And their `bound_integrable` used `integrable_log_over_pow (r := -s.re/2) (by linarith) Npos` — with N = 1.\n\nRather than guess, let me read their exact hF_meas for the measurability pattern and copy the whole proof structure with my modifications. I already have the full text from the earlier sed (lines 949-1040ish). Let me now write §3 based on it.\n\nActually — one simplification: my F z x := (x:ℂ)^(−z−2) * f x — with f = ↑b2Fun. The integrability of F s (Integrable (F s) μ): my hInt2-style: IntegrableOn ↑b2Fun·x^(−s−2) — but F's order is x^... * f (reversed) — congr.\n\nLet me write §3 as a near-verbatim clone with the three modifications (ε, bound exponent, f continuous-measurable). And note hF_meas needs ∀ᶠ z near s: AEStronglyMeasurable (F z) μ — via: for z near s (re z > −1): the integrand integrable... their hF_meas used integrableOn_of_Zeta0_fun for ALL z with re z > 0 (the nhds set). Mine: for z with re z > −1: IntegrableOn of ↑b2Fun·x^(−z−2) — that's my hInt2 proof generalized to (hz : −1 < z.re) — let me factor hInt2 as a standalone lemma `integrableOn_b2_cpow {s : ℂ} (hs : -1 < s.re) : IntegrableOn (fun x => (b2Fun x:ℂ) * (x:ℂ)^(-s-2)) (Ioi 1)` — extract from integral_b1_cpow_eq's hInt2 (which has hs : 0 < s.re — generalize to −1 < s.re: the proof only used s.re > −1 ✓).\n\nRestructure: make `integrableOn_b2_cpow` a standalone theorem with (−1 < s.re), and integral_b1_cpow_eq uses it. Same for the log-integrand: IntegrableOn (fun x => ↑b2Fun x * x^(−s−2)·(−log x)) (Ioi 1) — the log factor: |log x| ≤ ... on Ioi 1: |log x| ≤ x^ε·C — for the bound: ‖↑b2Fun·x^(−s−2)·log x‖ ≤ (1/8)·x^(−σ−2)·log x: integrable via integrable_log_over_pow (r := −σ−1 < 0 ✓ since σ > −1): their lemma gives IntegrableOn (‖x^(r−1)‖·‖log x‖) (Ioi N) with r−1 = −σ−2 ⟹ r = −σ−1 < 0 ✓. So:\n```lean\ntheorem integrableOn_b2_cpow_log {s : ℂ} (hs : -1 < s.re) :\n    IntegrableOn (fun x : ℝ => (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) * (-Real.log x))) (Set.Ioi 1) := by\n  have hg : IntegrableOn (fun x : ℝ => x ^ (-s.re - 2) * Real.log x) (Set.Ioi 1) := by\n    have := integrable_log_over_pow (r := -s.re - 1) (by linarith) (N := 1) (by norm_num)\n    -- their form: ‖x^(r−1)‖·‖log x‖ = x^(−σ−2)·|log x|: convert\n    ...\n```\nintegrable_log_over_pow gives IntegrableOn (fun x => ‖x^(r−1)‖ * ‖Real.log x‖) (Ioi ↑1): ‖x^(r−1)‖ = x^(r−1) (rpow_nonneg): with r = −σ−1: r−1 = −σ−2 ✓. So hg: IntegrableOn (fun x => x^(−σ−2)·|log x|). Then mono' with my integrand: ‖↑b2Fun·x^(−s−2)·(−log x)‖ = |b2Fun|·x^(−σ−2)·|log x| ≤ (1/8)·x^(−σ−2)|log x| ≤ x^(−σ−2)|log x| ✓.\n\nOK let me now write §3 fully. I'll restructure: extract integrableOn_b2_cpow as standalone, add integrableOn_b2_cpow_log, then hasDerivAt_b2Integral.\n\nOne important detail — in integral_b1_cpow_eq, replace the inline hInt2 with the standalone lemma call. Let me restructure via edits: add the two standalone integrability theorems BEFORE integral_b1_cpow_eq, and replace its inline hInt2 with a call.","signature":""},{"type":"text","text":"Now §3. First, extracting the B̃₂-integrability as standalone lemmas (needed in more general form for the analyticity proof)."},{"type":"tool_use","id":"Edit_251","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiRBound.lean","old_string":"/-- **The level-2 Euler–Maclaurin identity** (re s > 0):\n∫₁^∞ B̃₁·x^{−s−1} = (s+1)·∫₁^∞ B̃₂·x^{−s−2}. -/\ntheorem integral_b1_cpow_eq {s : ℂ} (hs : 0 < s.re) :\n    ∫ x in Set.Ioi (1:ℝ), (B1 x : ℂ) * (x : ℂ) ^ (-s - 1)\n      = (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by\n  have hInt1 : IntegrableOn (fun x : ℝ => (B1 x : ℂ) * (x : ℂ) ^ (-s - 1)) (Set.Ioi 1) := by\n    have h := (integrableOn_of_Zeta0_fun (N := 1) (by norm_num) (s := s) hs).neg\n    rw [Nat.cast_one] at h\n    apply IntegrableOn.congr_fun h _ measurableSet_Ioi\n    intro x hx\n    have hx0 : (0:ℝ) ≤ x := zero_le_one.trans (Set.mem_Ioi.mp hx).le\n    simp only [Pi.neg_apply]\n    rw [b1_eq_fract_sub_half hx0, Int.fract]\n    have e : (-(s + 1) : ℂ) = -s - 1 := by ring\n    rw [e]\n    push_cast\n    ring\n  have hInt2 : IntegrableOn (fun x : ℝ => (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) (Set.Ioi 1) := by\n    have hg : IntegrableOn (fun x : ℝ => x ^ (-s.re - 2)) (Set.Ioi 1) :=\n      integrableOn_Ioi_rpow_of_lt (show -s.re - 2 < -1 by linarith) one_pos\n    have hmeas : AEStronglyMeasurable (fun x : ℝ => (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2))\n        (volume.restrict (Set.Ioi (1:ℝ))) := by\n      apply ContinuousOn.aestronglyMeasurable _ measurableSet_Ioi\n      apply ContinuousOn.mul\n      · exact (continuous_ofReal.comp continuous_b2Fun).continuousOn\n      · intro x hx\n        exact (continuousAt_ofReal_cpow_const x _\n          (Or.inr (by linarith [Set.mem_Ioi.mp hx] : x ≠ 0))).continuousWithinAt\n    have hbound : ∀ᵐ x ∂(volume.restrict (Set.Ioi 1)),\n        ‖(b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖ ≤ x ^ (-s.re - 2) := by\n      filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n      have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx\n      have hnorm : ‖(x : ℂ) ^ (-s - 2)‖ = x ^ (-s.re - 2) := by\n        rw [norm_cpow_eq_rpow_re_of_pos (by linarith)]\n        congr 2\n      rw [norm_mul, Complex.norm_real, hnorm]\n      calc |b2Fun x| * x ^ (-s.re - 2)\n          ≤ (1 / 8) * x ^ (-s.re - 2) :=\n            mul_le_mul_of_nonneg_right (abs_b2Fun_le x) (Real.rpow_nonneg (by linarith) _)\n        _ ≤ x ^ (-s.re - 2) :=\n            mul_le_of_le_one_left (Real.rpow_nonneg (by linarith) _) (by norm_num)\n    exact Integrable.mono' hg hmeas hbound\n  have hT1 := intervalIntegral_tendsto_integral_Ioi (a := (1:ℝ)) (b := fun N : ℕ => (N : ℝ))\n    hInt1 tendsto_natCast_atTop_atTop\n  have hT2 := intervalIntegral_tendsto_integral_Ioi (a := (1:ℝ)) (b := fun N : ℕ => (N : ℝ))\n    hInt2 tendsto_natCast_atTop_atTop","new_string":"/-- The B̃₂·x^{−s−2} integrand is integrable on (1, ∞) for re s > −1. -/\ntheorem integrableOn_b2_cpow {s : ℂ} (hs : -1 < s.re) :\n    IntegrableOn (fun x : ℝ => (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) (Set.Ioi 1) := by\n  have hg : IntegrableOn (fun x : ℝ => x ^ (-s.re - 2)) (Set.Ioi 1) :=\n    integrableOn_Ioi_rpow_of_lt (show -s.re - 2 < -1 by linarith) one_pos\n  have hmeas : AEStronglyMeasurable (fun x : ℝ => (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2))\n      (volume.restrict (Set.Ioi (1:ℝ))) := by\n    apply ContinuousOn.aestronglyMeasurable _ measurableSet_Ioi\n    apply ContinuousOn.mul\n    · exact (continuous_ofReal.comp continuous_b2Fun).continuousOn\n    · intro x hx\n      exact (continuousAt_ofReal_cpow_const x _\n        (Or.inr (by linarith [Set.mem_Ioi.mp hx] : x ≠ 0))).continuousWithinAt\n  have hbound : ∀ᵐ x ∂(volume.restrict (Set.Ioi 1)),\n      ‖(b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖ ≤ x ^ (-s.re - 2) := by\n    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n    have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx\n    have hnorm : ‖(x : ℂ) ^ (-s - 2)‖ = x ^ (-s.re - 2) := by\n      rw [norm_cpow_eq_rpow_re_of_pos (by linarith)]\n      congr 2\n    rw [norm_mul, Complex.norm_real, hnorm]\n    calc |b2Fun x| * x ^ (-s.re - 2)\n        ≤ (1 / 8) * x ^ (-s.re - 2) :=\n          mul_le_mul_of_nonneg_right (abs_b2Fun_le x) (Real.rpow_nonneg (by linarith) _)\n      _ ≤ x ^ (-s.re - 2) :=\n          mul_le_of_le_one_left (Real.rpow_nonneg (by linarith) _) (by norm_num)\n  exact Integrable.mono' hg hmeas hbound\n\n/-- The log-weighted B̃₂ integrand is integrable on (1, ∞) for re s > −1. -/\ntheorem integrableOn_b2_cpow_log {s : ℂ} (hs : -1 < s.re) :\n    IntegrableOn (fun x : ℝ => (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) * (-Real.log x)))\n      (Set.Ioi 1) := by\n  have hg : IntegrableOn (fun x : ℝ => x ^ (-s.re - 2) * |Real.log x|) (Set.Ioi 1) := by\n    have h := integrable_log_over_pow (r := -s.re - 1) (by linarith) (N := 1) (by norm_num)\n    rw [Nat.cast_one] at h\n    refine h.congr_fun ?_ measurableSet_Ioi\n    intro x hx\n    have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx\n    rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _),\n      abs_of_nonneg (by linarith : (0:ℝ) ≤ Real.log x)]\n    congr 2\n    ring\n  have hmeas : AEStronglyMeasurable (fun x : ℝ => (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) *\n      (-Real.log x))) (volume.restrict (Set.Ioi (1:ℝ))) := by\n    apply ContinuousOn.aestronglyMeasurable _ measurableSet_Ioi\n    apply ContinuousOn.mul\n    · exact (continuous_ofReal.comp continuous_b2Fun).continuousOn\n    · apply ContinuousOn.mul\n      · intro x hx\n        exact (continuousAt_ofReal_cpow_const x _\n          (Or.inr (by linarith [Set.mem_Ioi.mp hx] : x ≠ 0))).continuousWithinAt\n      · apply Continuous.neg _).continuousOn  -- −log x: continuous on Ioi 1\n        -- (continuous_neg (Real.log ∘ ...)): use:\n        exact (continuous_neg_of... ) sorry\n  sorry\n\n/-- **The level-2 Euler–Maclaurin identity** (re s > 0):\n∫₁^∞ B̃₁·x^{−s−1} = (s+1)·∫₁^∞ B̃₂·x^{−s−2}. -/\ntheorem integral_b1_cpow_eq {s : ℂ} (hs : 0 < s.re) :\n    ∫ x in Set.Ioi (1:ℝ), (B1 x : ℂ) * (x : ℂ) ^ (-s - 1)\n      = (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by\n  have hInt1 : IntegrableOn (fun x : ℝ => (B1 x : ℂ) * (x : ℂ) ^ (-s - 1)) (Set.Ioi 1) := by\n    have h := (integrableOn_of_Zeta0_fun (N := 1) (by norm_num) (s := s) hs).neg\n    rw [Nat.cast_one] at h\n    apply IntegrableOn.congr_fun h _ measurableSet_Ioi\n    intro x hx\n    have hx0 : (0:ℝ) ≤ x := zero_le_one.trans (Set.mem_Ioi.mp hx).le\n    simp only [Pi.neg_apply]\n    rw [b1_eq_fract_sub_half hx0, Int.fract]\n    have e : (-(s + 1) : ℂ) = -s - 1 := by ring\n    rw [e]\n    push_cast\n    ring\n  have hT1 := intervalIntegral_tendsto_integral_Ioi (a := (1:ℝ)) (b := fun N : ℕ => (N : ℝ))\n    hInt1 tendsto_natCast_atTop_atTop\n  have hT2 := intervalIntegral_tendsto_integral_Ioi (a := (1:ℝ)) (b := fun N : ℕ => (N : ℝ))\n    (integrableOn_b2_cpow (by linarith)) tendsto_natCast_atTop_atTop"},"extra_content":null}]