[{"type":"thinking","thinking":"`MeasureTheory.Integrable.mono' {f : α → β} {g : α → ℝ} (hg : Integrable g μ) (hf : AEStronglyMeasurable f μ) (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ g x) : Integrable f μ` — it's on `Integrable` (not IntegrableOn). For IntegrableOn: work via restrict: `IntegrableOn f s μ ↔ Integrable f (μ.restrict s)` — `integrableOn_iff...`? There's `IntegrableOn` def as Integrable on restrict ✓ (`IntegrableOn f s μ := Integrable f (μ.restrict s)` by definition!). So:\n\n```lean\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    apply Integrable.mono' (by ...) ...\n```\nHmm — IntegrableOn.mono' doesn't exist; do: `rw [IntegrableOn]` hmm IntegrableOn is a def — `IntegrableOn f s μ` unfolds to Integrable f (μ.restrict s)? There's `integrableOn_def`? Just use: `show Integrable _ (volume.restrict (Set.Ioi 1))` — is IntegrableOn reducible? It's `def IntegrableOn ... := Integrable f (μ.restrict s)` — `show` should work (defeq). Then Integrable.mono' with hg restricted: hg : IntegrableOn g (Ioi 1) volume = Integrable g (volume.restrict (Ioi 1)) ✓ defeq too:\n\n```lean\n    refine (Integrable.mono' hg ?_ ?_ : Integrable _ _)\n```\nwith hg coerced... let me write:\n\n```lean\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    refine IntegrableOn.congr_fun (Integrable.mono' hg ?_ ?_) ?_ measurableSet_Ioi\n    · -- AEStronglyMeasurable (fun x => ↑b2Fun x * ↑x^(−s−2)) (volume.restrict (Ioi 1))\n      exact ((continuous_ofReal.comp continuous_b2Fun).continuousOn.mul\n        (fun x hx => (continuousAt_ofReal_cpow_const x _\n          (Or.inr (ne_of_gt (Set.mem_Ioi.mp hx)))).continuousWithinAt)).aestronglyMeasurable\n        measurableSet_Ioi\n    · filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n      -- ‖↑b2Fun x * ↑x^(−s−2)‖ ≤ x^(−σ−2)\n      ...\n    · intro x hx; rfl  -- EqOn rfl\n```\nHmm — Integrable.mono' hg : AEStronglyMeasurable f _ → (∀ᵐ ... ‖f‖ ≤ g) → Integrable f (restrict) — then congr_fun to... wait no — the f in mono' IS my function already: refine Integrable.mono' hg ?meas ?bound — produces Integrable (my f) (restrict) = IntegrableOn my f ✓ directly (defeq). No congr_fun needed:\n```lean\n    exact Integrable.mono' hg ?meas ?bound\n```\nwith the result type unifying IntegrableOn ↔ Integrable-on-restrict by defeq in `exact`. Hmm — IntegrableOn is a def not an abbrev — defeq unfolding should work with exact? `IntegrableOn` is defined via def — Lean unfolds defs during typechecking (reducible? default) — `exact` uses isDefEq which unfolds regular defs ✓ should work. If not: `rw [integrableOn_iff_integrable_restrict]`? hmm — hmm there's `integrableOn_iff_integrable_restrict`? or just `show Integrable _ _`. I'll write `show Integrable _ (volume.restrict _)` if needed. Let me structure:\n\n```lean\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)) :=\n      ((continuous_ofReal.comp continuous_b2Fun).continuousOn.mul\n        (fun x hx => (continuousAt_ofReal_cpow_const x _\n          (Or.inr (ne_of_gt (Set.mem_Ioi.mp hx)))).continuousWithinAt)).aestronglyMeasurable\n        measurableSet_Ioi\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        simp\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```\nThe final exact: Integrable.mono' hg hmeas hbound : Integrable mine (restrict) — vs goal IntegrableOn mine (Ioi 1) volume — defeq ✓ hope. If not, add `show Integrable _ _` first.\n\nHmm — also the mul_le_of_le_one_left : 0 ≤ b → a ≤ 1 → a*b ≤ b? signature: `mul_le_of_le_one_left (hb : 0 ≤ b) (ha : a ≤ 1) : a * b ≤ b` ✓.\n\nAnd (1/8 : ℝ) ≤ 1 by norm_num ✓.\n\nLet me now rewrite the hInt1/hInt2 + the whole tail (with the fixed induction) as one clean replacement. Also fix intervalIntegrable_b1_mul_cpow / b2 helper + the induction step. Big edit — replace from \"/-- Product integrability\" through the end of integral_b1_cpow_eq.","signature":""},{"type":"text","text":"Rewriting §2's tail cleanly (helpers + N-sum + limit) with the corrected API calls."},{"type":"tool_use","id":"Edit_240","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiRBound.lean","old_string":"/-- 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).neg\n    refine h.congr_fun ?_ measurableSet_Ioi\n    intro x hx\n    have hx0 : (0:ℝ) ≤ x := (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    apply IntegrableOn.mono' (integrableOn_Ioi_rpow_of_lt\n      (show -s.re - 2 < -1 by linarith) one_pos)\n    · exact ((continuous_ofReal.comp continuous_b2Fun).continuousOn.aestronglyMeasurable\n        measurableSet_Ioi).mul\n        ((fun x hx => (continuousAt_ofReal_cpow_const x _\n          (Or.inr (ne_of_gt (Set.mem_Ioi.mp hx)))).continuousWithinAt :\n            ContinuousOn (fun x : ℝ => (x : ℂ) ^ (-s - 2)) (Set.Ioi 1)).aestronglyMeasurable\n              measurableSet_Ioi)\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        simp\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  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\n  have heq : ∀ᶠ N : ℕ in atTop,\n      (∫ x in (1:ℝ)..(N : ℝ), (B1 x : ℂ) * (x : ℂ) ^ (-s - 1))\n        = (s + 1) * ∫ x in (1:ℝ)..(N : ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by\n    filter_upwards [Filter.eventually_atTop.mpr ⟨1, fun N hN =>\n      intervalIntegral_b1_cpow_nat N hN s (fun h => by\n        have : s.re = -1 := by rw [h]; simp\n        linarith)⟩] with N hN\n    exact hN\n  exact tendsto_nhds_unique (hT1.congr' heq) (hT2.const_mul (s + 1))","new_string":"/-- 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 := by\n  apply (intervalIntegrable_b1 ha.le hab).mul_continuousOn\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_b2_mul_cpow (c : ℂ) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :\n    IntervalIntegrable (fun x : ℝ => (b2Fun x : ℂ) * (x : ℂ) ^ c) volume a b := by\n  apply IntervalIntegrable.mul_continuousOn\n  · exact (continuous_ofReal.comp continuous_b2Fun).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/-- 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 hsucc : ((N + 1 : ℕ) : ℝ) = (N : ℝ) + 1 := by push_cast; ring\n      rw [hsucc]\n      have hN1 : (1:ℝ) ≤ (N : ℝ) := by exact_mod_cast hNpos\n      have hNN : (N : ℝ) ≤ (N : ℝ) + 1 := by linarith\n      have hN0R : (0:ℝ) < (N : ℝ) := by exact_mod_cast hNpos\n      rw [← intervalIntegral.integral_add_adjacent_intervals\n        (intervalIntegrable_b1_mul_cpow (-s - 1) one_pos hN1)\n        (intervalIntegrable_b1_mul_cpow (-s - 1) hN0R hNN)]\n      rw [ih hNpos, intervalIntegral_b1_cpow N hNpos s hs]\n      rw [← intervalIntegral.integral_add_adjacent_intervals\n        (intervalIntegrable_b2_mul_cpow (-s - 2) one_pos hN1)\n        (intervalIntegrable_b2_mul_cpow (-s - 2) hN0R hNN)]\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).neg\n    apply IntegrableOn.congr_fun h _ measurableSet_Ioi\n    intro x hx\n    have hx0 : (0:ℝ) ≤ x := (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)) :=\n      ((continuous_ofReal.comp continuous_b2Fun).continuousOn.mul\n        (fun x hx => (continuousAt_ofReal_cpow_const x _\n          (Or.inr (ne_of_gt (Set.mem_Ioi.mp hx)))).continuousWithinAt)).aestronglyMeasurable\n        measurableSet_Ioi\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        simp\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\n  have heq : ∀ᶠ N : ℕ in atTop,\n      (∫ x in (1:ℝ)..(N : ℝ), (B1 x : ℂ) * (x : ℂ) ^ (-s - 1))\n        = (s + 1) * ∫ x in (1:ℝ)..(N : ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by\n    filter_upwards [Filter.eventually_atTop.mpr ⟨1, fun N hN =>\n      intervalIntegral_b1_cpow_nat N hN s (fun h => by\n        have : s.re = -1 := by rw [h]; simp\n        linarith)⟩] with N hN\n    exact hN\n  exact tendsto_nhds_unique (hT1.congr' heq) (hT2.const_mul (s + 1))"},"extra_content":null}]