[{"type":"thinking","thinking":"- `IntervalIntegrable.mul_continuousOn (hf : IntervalIntegrable f μ a b) (hg : ContinuousOn g [[a,b]]) : IntervalIntegrable (fun x => f x * g x)` ✓ — f = ↑B1 (integrable), g = cpow (continuous) gives ↑B1·cpow ✓ (order matches our form (B1 x)·(x^..) ✓).\n\nNow write the rest of §2: the N-sum + Ioi limit identity. Also §3/§4/§5. Let me write §2's remainder now:\n\n```lean\n/-- The IBP identity summed to [1, N] (natural N ≥ 1). -/\ntheorem intervalIntegral_b1_cpow_nat (N : ℕ) (hN : 1 ≤ N) (s : ℂ) (hs : s ≠ -1) :\n    ∫ x in (1:ℝ)..(N : ℝ), (B1 x : ℂ) * (x : ℂ) ^ (-s - 1)\n      = (s + 1) * ∫ x in (1:ℝ)..(N : ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by\n  induction N with\n  | zero => exact absurd hN (by norm_num)\n  | succ N ih =>\n    rcases Nat.eq_zero_or_pos N with hN0 | hNpos\n    · subst hN0\n      simp\n    · have hI1 : IntervalIntegrable (fun x : ℝ => (B1 x : ℂ) * (x : ℂ) ^ (-s - 1)) volume 1 (N : ℝ) := by\n        apply IntervalIntegrable.mul_continuousOn (f := fun x : ℝ => (B1 x : ℂ)) ...\n```\nHmm — the IntervalIntegrable of ↑B1 on [1, N]: extract from hu'int? hu'int was on [k, k+1]. General [1, N]: same bounded-ae argument: let me make a standalone helper:\n\n```lean\ntheorem intervalIntegrable_b1 (a b : ℝ) : IntervalIntegrable (fun x : ℝ => (B1 x : ℂ)) volume a b := by\n  rw [intervalIntegrable_iff']\n  apply MeasureTheory.Measure.integrableOn_of_bounded (by simp) (by fun_prop) (M := 1 / 2)\n  filter_upwards [self_mem_ae_restrict (by measurability)] with x hx\n  rw [Complex.norm_real]\n  -- |B1 x| ≤ 1/2 needs 0 ≤ x — uIcc a b could contain negatives!\n```\nabs_B1_le_half needs 0 ≤ x. For a general [a,b] with negatives, B1 x = x − ⌊x⌋₊ − 1/2 with ⌊x⌋₊ = 0 for x < 0: |B1 x| = |x − 1/2| — unbounded on big negatives! But our intervals are within [1, ∞): state `intervalIntegrable_b1 (ha : 1 ≤ a) (a b : ℝ)`? Just require 1 ≤ a, a ≤ b. Or bound differently for x < 0... Simplest: hypothesis 0 ≤ a:\n```lean\ntheorem intervalIntegrable_b1 {a b : ℝ} (ha : 0 ≤ a) :\n    IntervalIntegrable (fun x : ℝ => (B1 x : ℂ)) volume a b := by\n  rw [intervalIntegrable_iff']\n  -- handle a > b: uIcc\n  apply MeasureTheory.Measure.integrableOn_of_bounded (by simp) (by fun_prop) (M := max (1/2) (|b| + 1))... \n```\nhmm — x ∈ uIcc a b: x ≥ min a b = a ≥ 0 (if a ≤ b)... uIcc handles both orders: x ≥ min a b; if a ≤ b: min = a ≥ 0 ✓. Just require 0 ≤ a ∧ a ≤ b? For our uses: intervals [1, N], [N, N+1], [k, k+1] all ordered. State (ha : 0 ≤ a) (hab : a ≤ b):\n```lean\ntheorem intervalIntegrable_b1 {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) :\n    IntervalIntegrable (fun x : ℝ => (B1 x : ℂ)) volume a b := by\n  rw [intervalIntegrable_iff']\n  rw [Set.uIcc_of_le hab]  -- hmm intervalIntegrable_iff' puts it on uIcc\n  apply MeasureTheory.Measure.integrableOn_of_bounded (by simp) (by fun_prop) (M := 1 / 2)\n  filter_upwards [self_mem_ae_restrict (by measurability)] with x hx\n  rw [Complex.norm_real]\n  exact abs_B1_le_half (hx.1.trans? ...)  -- hx : x ∈ Icc a b: a ≤ x: 0 ≤ x ✓ linarith [hx.1]\n```\nHmm — does `intervalIntegrable_iff'` produce IntegrableOn ... (uIcc a b)? From their usage: rw [intervalIntegrable_iff'] then integrableOn_of_bounded — the goal becomes IntegrableOn f (volume.restrict (uIcc a b))? then apply integrableOn_of_bounded — the (by simp) discharges μ s < ∞ — with s = uIcc a b ✓. And self_mem_ae_restrict (by measurability) gives x ∈ uIcc: rw uIcc_of_le at hx ✓ then hx.1 : a ≤ x.\n\nAnd the cpow continuous integrability:\n```lean\ntheorem intervalIntegrable_cpow (c : ℂ) {a b : ℝ} (ha : 0 < a) :\n    IntervalIntegrable (fun x : ℝ => (x : ℂ) ^ c) volume a b := by\n  apply ContinuousOn.intervalIntegrable\n  rw [Set.uIcc_of_le (ha.le.trans?? ...)]  -- need a ≤ b... \n```\nHmm — IntervalIntegrable's ContinuousOn.intervalIntegrable: `ContinuousOn.intervalIntegrable (h : ContinuousOn f [[a,b]]) : IntervalIntegrable f volume a b`? — it takes uIcc — no a ≤ b needed ✓. ContinuousOn on uIcc a b: points x ≥ min a b = a (if a ≤ b) — for a > b: uIcc = [b, a]: x ≥ b — could be ≤ 0! Our uses are ordered; keep it simple: (ha : 0 < a) (hab : a ≤ b):\n```lean\ntheorem intervalIntegrable_cpow (c : ℂ) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :\n    IntervalIntegrable (fun x : ℝ => (x : ℂ) ^ c) volume a b := by\n  apply ContinuousOn.intervalIntegrable\n  rw [Set.uIcc_of_le hab]\n  intro x hx\n  exact (continuousAt_ofReal_cpow_const x _ (Or.inr (by linarith [hx.1]))).continuousWithinAt\n```\nThen the products:\n```lean\ntheorem intervalIntegrable_b1_mul_cpow (c : ℂ) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :\n    IntervalIntegrable (fun x : ℝ => (B1 x : ℂ) * (x : ℂ) ^ c) volume a b :=\n  (intervalIntegrable_b1 ha.le hab).mul_continuousOn (c := ...)  -- g := cpow: ContinuousOn g [[a,b]]\n```\nHmm — mul_continuousOn (hg : ContinuousOn g [[a,b]]) : IntervalIntegrable (f x * g x): the cpow's ContinuousOn on uIcc: same as above.\n\nActually wait — the uIcc forms in these lemmas vs the `Set.uIcc_of_le` — `ContinuousOn.intervalIntegrable` — the ContinuousOn hypothesis is on [[a,b]] = uIcc ✓.\n\nOK writing the rest of §2 now (helpers + N-sum + Ioi limit), then §3, §4, §5. Let me write §2's completion first and compile.","signature":""},{"type":"text","text":"Now writing §2's completion (helpers, N-sum, Ioi limit)."},{"type":"tool_use","id":"Edit_231","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiRBound.lean","old_string":"  rw [intervalIntegral.integral_const_mul] at hIBP\n  rw [neg_mul] at hIBP\n  exact (neg_inj.mp hIBP).symm\n\nend NguyenRH1\n\nend","new_string":"  rw [intervalIntegral.integral_const_mul] at hIBP\n  rw [neg_mul] at hIBP\n  exact (neg_inj.mp hIBP).symm\n\n/-- B̃₁ is interval-integrable on any interval in [0, ∞). -/\ntheorem intervalIntegrable_b1 {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) :\n    IntervalIntegrable (fun x : ℝ => (B1 x : ℂ)) volume a b := by\n  rw [intervalIntegrable_iff', Set.uIcc_of_le hab]\n  apply MeasureTheory.Measure.integrableOn_of_bounded (by simp) (by fun_prop) (M := 1 / 2)\n  filter_upwards [self_mem_ae_restrict (by measurability)] with x hx\n  rw [Complex.norm_real]\n  exact abs_B1_le_half (by linarith [hx.1])\n\n/-- The ofReal-cpow is interval-integrable on intervals in (0, ∞). -/\ntheorem intervalIntegrable_cpow (c : ℂ) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :\n    IntervalIntegrable (fun x : ℝ => (x : ℂ) ^ c) volume a b := by\n  apply ContinuousOn.intervalIntegrable\n  rw [Set.uIcc_of_le hab]\n  intro x hx\n  exact (continuousAt_ofReal_cpow_const x _ (Or.inr (by linarith [hx.1]))).continuousWithinAt\n\n/-- Product integrability: B̃₁·x^c on intervals in (0, ∞). -/\ntheorem intervalIntegrable_b1_mul_cpow (c : ℂ) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :\n    IntervalIntegrable (fun x : ℝ => (B1 x : ℂ) * (x : ℂ) ^ c) volume a b :=\n  (intervalIntegrable_b1 ha.le hab).mul_continuousOn\n    (continuousOn_of_continuousAt fun x hx =>\n      (continuousAt_ofReal_cpow_const x _ (Or.inr (by\n        rw [Set.uIcc_of_le hab] at hx\n        linarith [hx.1]))).continuousWithinAt)\n\n/-- The IBP identity summed to [1, N] (natural N ≥ 1). -/\ntheorem intervalIntegral_b1_cpow_nat (N : ℕ) (hN : 1 ≤ N) (s : ℂ) (hs : s ≠ -1) :\n    ∫ x in (1:ℝ)..(N : ℝ), (B1 x : ℂ) * (x : ℂ) ^ (-s - 1)\n      = (s + 1) * ∫ x in (1:ℝ)..(N : ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by\n  induction N with\n  | zero => exact absurd hN (by norm_num)\n  | succ N ih =>\n    rcases Nat.eq_zero_or_pos N with hN0 | hNpos\n    · subst hN0\n      simp\n    · have h1 : (0:ℝ) < (1:ℝ) := one_pos\n      have hsucc : ((N + 1 : ℕ) : ℝ) = (N : ℝ) + 1 := by push_cast; ring\n      rw [hsucc]\n      rw [← intervalIntegral.integral_add_adjacent_intervals\n        (intervalIntegrable_b1_mul_cpow (-s - 1) one_pos (by exact_mod_cast hNpos))\n        (intervalIntegrable_b1_mul_cpow (-s - 1) (by exact_mod_cast hNpos) (by linarith))]\n      rw [ih hNpos, intervalIntegral_b1_cpow N hNpos s hs]\n      have h2 : IntervalIntegrable (fun x : ℝ => (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) volume\n          (1 : ℝ) (N : ℝ) :=\n        (continuous_b2Fun.ofReal).continuousOn.intervalIntegrable.mul_continuousOn\n          (continuousOn_of_continuousAt fun x hx =>\n            (continuousAt_ofReal_cpow_const x _ (Or.inr (by\n              rw [Set.uIcc_of_le (by exact_mod_cast hNpos : (1:ℝ) ≤ (N:ℝ))] at hx\n              linarith [hx.1]))).continuousWithinAt)\n      have h3 : IntervalIntegrable (fun x : ℝ => (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) volume\n          (N : ℝ) ((N : ℝ) + 1) :=\n        (continuous_b2Fun.ofReal).continuousOn.intervalIntegrable.mul_continuousOn\n          (continuousOn_of_continuousAt fun x hx =>\n            (continuousAt_ofReal_cpow_const x _ (Or.inr (by\n              rw [Set.uIcc_of_le (by linarith : (N:ℝ) ≤ (N:ℝ) + 1)] at hx\n              have : (N : ℝ) ≤ x := hx.1\n              have hN0 : (0:ℝ) < N := by exact_mod_cast hNpos\n              linarith))).continuousWithinAt)\n      rw [← intervalIntegral.integral_add_adjacent_intervals h2 h3]\n      ring\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\n    -- their integrand: (⌊x⌋ + 1/2 - x) * (x:ℂ)^(-(s+1)) = −B̃₁·x^{−s−1}\n    have heq : (fun x : ℝ => (B1 x : ℂ) * (x : ℂ) ^ (-s - 1))\n        = fun x : ℝ => -((⌊x⌋₊ + 1 / 2 - x : ℝ) : ℂ) * (x : ℂ) ^ (-(s + 1)) := by\n      funext x\n      rw [B1]\n      push_cast\n      ring_nf\n    rw [heq]\n    -- integrable from theirs via neg + exponent form\n    have h' : IntegrableOn (fun x : ℝ => -(((⌊x⌋₊ : ℝ) + 1 / 2 - x : ℝ) : ℂ) * (x : ℂ) ^ (-(s + 1)))\n        (Set.Ioi 1) := by\n      apply IntegrableOn.neg\n      convert h using 1\n      ext x\n      push_cast\n      ring_nf\n    exact h'\n  sorry\n  sorry\n\nend NguyenRH1\n\nend"},"extra_content":null}]