[{"type":"thinking","thinking":"`Convex.linear_preimage (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) : Convex 𝕜 (f ⁻¹' s)` ✓ and `Complex.reCLM : ℂ →L[ℝ] ℝ` with reCLM_coe : (reCLM : ℂ →ₗ[ℝ] ℝ) = reLm. And `convex_Ioi (c) : Convex ℝ (Ioi c)` ✓ standard.\n\nSo:\n```lean\ntheorem convex_halfplane_re_gt (c : ℝ) : Convex ℝ {z : ℂ | c < z.re} := by\n  have h : {z : ℂ | c < z.re} = Complex.reLm ⁻¹' (Set.Ioi c) := rfl  -- reLm: ℂ →ₗ[ℝ] ℝ\n  rw [h]\n  exact (convex_Ioi c).linear_preimage _\n```\nHmm — {z | c < z.re} = reLm ⁻¹' Ioi c: rfl ✓ (reLm applies to re). `Complex.reLm`? the name: reCLM_coe mentions `reLm` — so `Complex.reLm : ℂ →ₗ[ℝ] ℝ`? Let me just use reCLM as the CLM and coerce: (convex_Ioi c).linear_preimage (Complex.reCLM : ℂ →ₗ[ℝ] ℝ)? — linear_preimage wants a LinearMap: ((reCLM : ℂ →ₗ[ℝ] ℝ)) via reCLM_coe ✓. And the set equality: reCLM ⁻¹' (Ioi c) = {z | c < z.re}: by reCLM_apply ✓ rfl should hold (preimage of Ioi c under (·.re) is {z | c < z.re} ✓ definitionally).\n\nIsPreconnected from Convex: `Convex.isPreconnected (h : Convex 𝕜 s) : IsPreconnected s` ✓.\n\nNow write §4 fully and carefully:\n\n```lean\n/-! ## 4. The level-2 representation of ζ on re s > −1 -/\n\n/-- The half-plane {c < re z} is convex. -/\ntheorem convex_halfplane_re_gt (c : ℝ) : Convex ℝ {z : ℂ | c < z.re} :=\n  (convex_Ioi c).linear_preimage ((Complex.reCLM : ℂ →ₗ[ℝ] ℝ))\n\ntheorem convex_halfplane_im_gt (c : ℝ) : Convex ℝ {z : ℂ | c < z.im} :=\n  (convex_Ioi c).linear_preimage ((Complex.imCLM : ℂ →ₗ[ℝ] ℝ))\n```\nNeed Complex.imCLM ✓ exists (next to reCLM).\n\nThen the main:\n```lean\n/-- The level-2 representation on W⁺ = {re > −1, im > 5}. -/\ntheorem riemannZeta_eq_level2_of_im_gt {s : ℂ} (hs : -1 < s.re) (hs5 : 5 < s.im) :\n    riemannZeta s = 1 / 2 + 1 / (s - 1)\n      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by\n  set W : Set ℂ := {z : ℂ | -1 < z.re ∧ 5 < z.im}\n  have hWopen : IsOpen W :=\n    (isOpen_lt continuous_const Complex.continuous_re).inter\n      (isOpen_lt continuous_const Complex.continuous_im)\n  have hWpre : IsPreconnected W :=\n    ((convex_halfplane_re_gt _).inter (convex_halfplane_im_gt _)).isPreconnected\n  have hf_an : AnalyticOnNhd ℂ riemannZeta W :=\n    (HolomorphicOn_riemannZeta.mono (fun z hz => by\n      intro h1\n      rw [h1] at hz\n      exact absurd hz.2 (by norm_num))).analyticOnNhd hWopen\n```\nHmm — HolomorphicOn_riemannZeta : HolomorphicOn ζ {s | s ≠ 1} — .mono needs {s ≠ 1} ⊆?? wait mono direction: HolomorphicOn f s, t ⊆ s ⟹ HolomorphicOn f t: `HolomorphicOn.mono (h : HolomorphicOn f s) (hst : t ⊆ s)`. So: HolomorphicOn_riemannZeta.mono (fun z hz => ...) where hz : z ∈ W and must produce z ∈ {s | s ≠ 1} i.e. z ≠ 1: z ∈ W ⟹ im z > 5 ⟹ z ≠ 1 (im 1 = 0):\n```lean\n    (HolomorphicOn_riemannZeta.mono (fun z hz => by\n      show z ≠ 1\n      intro h1\n      rw [h1] at hz\n      exact absurd hz.2 (by norm_num)))...\n```\nhz : z ∈ W = {−1 < re ∧ 5 < im}: hz.2 : 5 < (1:ℂ).im = 0 — norm_num at hz... `simp at hz`? (1:ℂ).im = 0 via Complex.one_im: hz.2 : 5 < Complex.im 1 — simp [Complex.one_im] at hz → 5 < 0 — exact membership... write: `have : (5:ℝ) < (0:ℝ) := by rw [h1] at hz; exact hz.2.trans_eq? ...` — simpler:\n```lean\n      intro h1\n      have := hz.2  -- 5 < z.im\n      rw [h1, Complex.one_im] at this\n      norm_num at this\n```\n✓. And HolomorphicOn.mono gives HolomorphicOn ζ W; then `.analyticOnNhd hWopen`?? — HolomorphicOn is DifferentiableOn — `(HolomorphicOn ...).analyticOnNhd hWopen` via DifferentiableOn.analyticOnNhd ✓.\n\n- hg_an: RHS analytic on W:\n```lean\n  have hJ_an : AnalyticOnNhd ℂ (fun s : ℂ => ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) W := by\n    apply DifferentiableOn.analyticOnNhd _ hWopen\n    intro z hz\n    exact (hasDerivAt_b2Integral hz.1).differentiableAt.differentiableWithinAt\n  have hg_an : AnalyticOnNhd ℂ (fun s : ℂ => 1 / 2 + 1 / (s - 1)\n      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) W := by\n    intro z hz\n    apply AnalyticAt.sub _ (hJ_an z hz)\n    apply AnalyticAt.add analyticAt_const\n    apply AnalyticAt.one_div (analyticAt_id.sub analyticAt_const)\n    intro h\n    have hz1 : z = 1 := by rwa [sub_eq_zero] at h  -- h : z − 1 = 0: sub_eq_zero : z − 1 = 0 ↔ z = 1 ✓\n    rw [hz1, Complex.one_im] at hz\n    exact absurd hz.2 (by norm_num)\n```\nHmm — AnalyticAt.one_div : AnalyticAt f z → f z ≠ 0 → AnalyticAt (fun w => 1 / f w) z? signature: `AnalyticAt.one_div (hf : AnalyticAt ℂ f z) (hg : f z ≠ 0) : AnalyticAt ℂ (fun x => 1 / f x) z`? hmm might be `.inv` or `one_div` — check: there's `AnalyticAt.inv` and `AnalyticAt.one_div`? I recall `AnalyticAt.one_div (hf : AnalyticAt 𝕜 f z) (hg : f z ≠ 0) : AnalyticAt 𝕜 (fun x => (f x)⁻¹?)...` — let me use `AnalyticAt.inv`... Actually `AnalyticAt.div analyticAt_const (sub) h`? 1/(s−1) = const/id−const: AnalyticAt.div (hf : AnalyticAt f) (hg : AnalyticAt g) (hg0 : g z ≠ 0) : AnalyticAt (f / g) — with f = 1: fun z => 1/(z−1) = (fun z => 1)/(fun z => z−1) pointwise ✓.\n\nAnd the sub: the function is (1/2 + 1/(s−1)) − s(s+1)·J(s): AnalyticAt.sub (add-part) (mul-part (hJ_an z hz)) ✓ with the mul-part: (analyticAt_id.mul (analyticAt_id.add analyticAt_const)).mul (hJ_an z hz) — the function s * (s+1) * J s: fun z => (z * (z+1)) * J z ✓ association ✓.\n\n- the eventuallyEq at basepoint 2+10i ∈ W:\n```lean\n  have hbase : (2 + 10 * Complex.I) ∈ W := by\n    constructor\n    · simp  -- re = 2 > −1\n    · simp  -- im = 10 > 5\n  have hEq : riemannZeta =ᶠ[𝓝 (2 + 10 * Complex.I)] (fun s : ℂ => 1/2 + 1/(s-1) - s*(s+1)*∫ ...) := by\n    -- on V ∩ 𝓝: V := {0 < re, ≠ 1} is a nhds of 2+10i:\n    have hV : {z : ℂ | 0 < z.re ∧ z ≠ 1} ∈ 𝓝 (2 + 10 * Complex.I) := by\n      rw [mem_nhds_iff]\n      exact ⟨{z | 0 < z.re ∧ z ≠ 1}, fun _ a ↦ a, \n        (isOpen_lt continuous_const Complex.continuous_re).inter (isOpen_ne' ?), by simp⟩\n    filter_upwards [hV] with z hz\n    exact riemannZeta_eq_level2_of_re_pos hz.1 hz.2\n  have hOn := (hf_an.eqOn_of_preconnected_of_eventuallyEq hg_an hWpre hbase hEq)  -- EqOn ζ RHS W\n  exact hOn s ⟨hs, hs5⟩\n```\n- `isOpen_ne'`? the set {z ≠ 1} open: `isOpen_ne`? For a single point complement: `isOpen_compl_singleton` ✓: {z | z ≠ 1} = {1}ᶜ: isOpen_compl_singleton ✓.\n- `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq` — signature from Zeta0EqZeta usage: `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq f_an g_an preconU h2 ?_ s_mem` — so (f_an) (g_an) (precon) (x∈U) (eventuallyEq) → returns EqOn... then `.symm` was applied — because their h gave agreement f = g and they wanted g = f. Note the eventualEq direction in their call: their ?_ was eventuallyEq at 2 of... they proved agreement ζ₀ = ζ on V via... whatever — I'll match my direction: hEq : riemannZeta =ᶠ RHS ⟹ eqOn : EqOn riemannZeta RHS W? The lemma: `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq (hf : AnalyticOnNhd ℂ f s) (hg : AnalyticOnNhd ℂ g s) (hs : IsPreconnected s) (hx : x ∈ s) (h : f =ᶠ[𝓝 x] g) : EqOn f g s` ✓ plausible. The result: EqOn ζ RHS W: at s: ζ s = RHS s ✓ my goal direction ✓ (goal: riemannZeta s = ...): hOn s ⟨hs, hs5⟩ : riemannZeta s = RHS s ✓.\n\nHmm — one catch: the analytic-side requirement — AnalyticOnNhd on W. Both analytic ✓.\n\nAnd the W⁻ version — identical with im < −5:\n- W⁻ := {−1 < re, im < −5}: open (isOpen_gt for im: isOpen_lt continuous_im continuous_const ✓); convex halfplane im < c: convex_halfplane_im_lt (c) via (convex_Iio c).linear_preimage imCLM ✓.\n- basepoint 2−10i.\n- z ≠ 1 from im < −5 ✓.\n\nAnd §5 the disc bound:\n```lean\n/-! ## 5. The polynomial bound on the disc B(2+it, 5/2) -/\n\ntheorem norm_riemannZeta_le_disc {t : ℝ} (ht : 10 ≤ |t|) {s : ℂ}\n    (hs : s ∈ Metric.closedBall ((2 : ℂ) + t * Complex.I) (5 / 2)) :\n    ‖riemannZeta s‖ ≤ 3 / 4 * |t| ^ 2 := by\n  -- geometry: re s ≥ −1/2 > −1; |im s| ≥ |t| − 5/2 ≥ 15/2 > 5\n  have hmem : ‖s - (2 + t * Complex.I)‖ ≤ 5 / 2 := by\n    rw [Metric.mem_closedBall, Complex.dist_eq] at hs  -- hmm dist s (2+tI) = ‖s − (2+it)‖\n    exact hs\n  have hre : -1/2 ≤ s.re := by\n    have : |s.re - 2| ≤ ‖s - (2 + t * Complex.I)‖ := abs_re_le_norm _\n    -- s.re − 2 ∈ [−5/2, 5/2]\n    rw [sub_re] at this  -- (s − (2+tI)).re = s.re − 2\n    ...\n```\nThe re/im extraction: (s − (2+tI)).re = s.re − 2 (sub_re, ofNat_re, mul_re of t·I: (t*I).re = 0 ✓); (s − (2+tI)).im = s.im − t ✓. So |s.re − 2| ≤ 5/2 ⟹ s.re ≥ −1/2 ✓; |s.im − t| ≤ 5/2 ⟹ |im s| ≥ |t| − 5/2 ≥ 15/2 ✓ (reverse triangle: |im s| ≥ |t| − |im s − t| — |im s| ≥ |t| − |im s − t| ✓ via abs_sub_abs_le...).\n\nThen cases on t ≥ 0 / t < 0:\n- t ≥ 0: im s ≥ t − 5/2 ≥ 15/2 > 5 ⟹ apply riemannZeta_eq_level2_of_im_gt (re s ≥ −1/2 > −1 ✓).\n- t < 0: im s ≤ t + 5/2 ≤ −15/2 < −5 ⟹ of_im_lt version.\n\nThen the norm bound: ζ s = 1/2 + 1/(s−1) − s(s+1)J(s):\n‖ζ‖ ≤ 1/2 + 1/‖s−1‖ + ‖s‖‖s+1‖‖J‖.\n‖J‖ ≤ (1/8)/(re s + 1) ≤ 1/4: \n‖J‖ = ‖∫₁^∞ ↑b2Fun x·↑x^(−s−2)‖ ≤ ∫₁^∞ (1/8)·x^(−σ−2) dx = (1/8)·(1/(σ+1)):\n  - norm_integral: ‖∫ x in Ioi 1, f x‖ ≤ ∫ x in Ioi 1, ‖f x‖ — `norm_integral_le_integral_norm`? — for the set integral: `norm_integral_le_integral_norm (f)`? there's `norm_integral_le_integral_norm : ‖∫ x, f x ∂μ‖ ≤ ∫ x, ‖f x‖ ∂μ` ✓ (works for set-integral via restrict).\n  - ∫₁^∞ (1/8)x^(−σ−2) = (1/8)·∫₁^∞ x^(−σ−2) = (1/8)/(σ+1): the rpow integral: `integral_rpow_of_lt`? name: for Ioi: `integral_Ioi_rpow_of_lt (ha : a < -1) (hc : 0 < c) : ∫ x in Ioi c, x^a = -c^(a+1)/(a+1)`? hmm sign: ∫₁^∞ x^a dx = [x^{a+1}/(a+1)]₁^∞ = 0 − 1/(a+1) = −1/(a+1) = 1/|a+1| for a < −1 ✓ (a+1 < 0). With a = −σ−2, a+1 = −σ−1: ∫ = −1/(−σ−1) = 1/(σ+1) ✓. Let me check the name at compile: `integral_Ioi_rpow_of_lt`?\n  \n  Then: ‖ζ‖ ≤ 1/2 + 1/10 + ‖s‖‖s+1‖/4 ≤ 3/5 + (|t|+9/2)(|t|+11/2)/4 ≤ 3/4·t² for |t| ≥ 10: nlinarith after expansion: (|t|+9/2)(|t|+11/2)/4 = (t² + 10|t| + 99/4)/4 ≤ t²/4 + (10·|t|)/4 + 25/4... let me just give nlinarith the pieces: (|t|+9/2)(|t|+11/2) ≤ (3/4·t² − 3/5)·4 ⟺ t²+10|t|+24.75 ≤ 3t² − 2.4 ⟺ 2t² − 10|t| − 27.15 ≥ 0 ⟸ |t| ≥ 10: 200 − 100 − 27 > 0 ✓ nlinarith [sq |t| etc.].\n\nDetails of ‖s‖ ≤ |t| + 9/2: ‖s‖ ≤ ‖s − (2+it)‖ + ‖2+it‖ ≤ 5/2 + (2+|t|) — ‖2+it‖ ≤ |re|+|im| = 2+|t| (Complex.norm_le_abs_re_add_abs_im ✓). ‖s+1‖ ≤ ‖s‖+1. ‖s−1‖ ≥ |im(s−1)| = |t| (abs_im_le_norm: |((s−1).im)| = |s.im| ≥ 15/2 hmm — 1/‖s−1‖ ≤ 1/(15/2) = 2/15 ≤ 1/10? — better: ‖s−1‖ ≥ |im(s−1)| = |s.im| ≥ 15/2 ⟹ 1/‖s−1‖ ≤ 2/15. Whatever — use 1/‖s−1‖ ≤ 2/15 (or 1/10 — 2/15 > 1/10! use 2/15). Constants: 1/2 + 2/15 + ... — fine, the 3/4 target has slack.\n\nOK — writing §4 + §5 now. This is the last big chunk of ii′-5b. Let me write §4 first (both im versions), compile, then §5.","signature":""},{"type":"text","text":"Writing §4 — representation on V (re > 0) then the W⁺/W⁻ extensions via the identity principle."},{"type":"tool_use","id":"Edit_281","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiRBound.lean","old_string":"/-! ## 4. The level-2 representation of ζ on re s > −1 -/\n\n/-- The level-2 representation on re s > 0: from Zeta23's `Zeta0EqZeta`\nplus the level-2 IBP identity. -/\ntheorem riemannZeta_eq_level2_of_re_pos {s : ℂ} (hs : 0 < s.re) (hs1 : s ≠ 1) :\n    riemannZeta s = 1 / 2 + 1 / (s - 1)\n      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by\n  have hs0 : s ≠ 0 := fun h => by rw [h] at hs; simp at hs\n  have h := Zeta0EqZeta (N := 1) (by norm_num) hs hs1\n  rw [← h]\n  rw [riemannZeta0_apply]\n  have hsum : ∑ n ∈ Finset.range (1 + 1), 1 / (n : ℂ) ^ s = 1 := by\n    rw [Finset.sum_range_succ, Finset.sum_range_one]\n    simp [Complex.zero_cpow hs0]\n  rw [hsum]\n  have hI1 : (∫ x in Set.Ioi ((1 : ℕ) : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1)))\n      = -∫ x in Set.Ioi (1:ℝ), (B1 x : ℂ) * (x : ℂ) ^ (-s - 1) := by\n    rw [← integral_neg]\n    apply integral_congr_ae\n    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n    have hx0 : (0:ℝ) ≤ x := zero_le_one.trans (Set.mem_Ioi.mp hx).le\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  rw [Nat.cast_one, hI1, integral_b1_cpow_eq hs]\n  field_simp\n  ring\n\n/-- The level-2 representation on the upper region W⁺ = {re > −1, im > 5}\n(convex, hence preconnected — the identity principle applies). -/\ntheorem riemannZeta_eq_level2_of_im_gt {s : ℂ} (hs : -1 < s.re) (hs5 : 5 < s.im) :\n    riemannZeta s = 1 / 2 + 1 / (s - 1)\n      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by\n  set W : Set ℂ := {z | -1 < z.re ∧ 5 < z.im}\n  have hWopen : IsOpen W :=\n    (isOpen_lt continuous_const Complex.continuous_re).inter\n      (isOpen_lt continuous_const Complex.continuous_im)\n  have hWpre : IsPreconnected W :=\n    ((convex_halfspace_re_gt _) -- hmm: {−1 < re}\n      |>.inter (convex_halfspace_im_gt _)).isPreconnected\n  -- LHS analytic on W (W avoids 1 since im > 5)\n  have hf_an : AnalyticOnNhd ℂ riemannZeta W :=\n    (HolomorphicOn_riemannZeta.mono (fun z hz => by\n      intro h1\n      rw [h1] at hz\n      simp at hz)).analyticOnNhd hWopen\n  -- RHS analytic on W\n  have hg_an : AnalyticOnNhd ℂ (fun s : ℂ => 1 / 2 + 1 / (s - 1)\n      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) W := by\n    intro z hz\n    apply AnalyticAt.sub\n    · apply AnalyticAt.add\n      · exact analyticAt_const\n      · apply AnalyticAt.one_div\n        · exact analyticAt_id.sub analyticAt_const\n        · intro h\n          have : z = 1 := by rwa [sub_eq_zero] at h\n          rw [this] at hz\n          simp at hz\n    · apply AnalyticAt.mul\n      · exact analyticAt_id.mul (analyticAt_id.add analyticAt_const)\n      · exact ((hasDerivAt_b2Integral hz.1).analyticAt ... )\n  sorry\n  sorry\n\nend NguyenRH1\n\nend","new_string":"/-! ## 4. The level-2 representation of ζ on re s > −1 -/\n\n/-- The half-plane {c < re z} is convex. -/\ntheorem convex_halfplane_re_gt (c : ℝ) : Convex ℝ {z : ℂ | c < z.re} :=\n  (convex_Ioi c).linear_preimage ((Complex.reCLM : ℂ →ₗ[ℝ] ℝ))\n\n/-- The half-plane {c < im z} is convex. -/\ntheorem convex_halfplane_im_gt (c : ℝ) : Convex ℝ {z : ℂ | c < z.im} :=\n  (convex_Ioi c).linear_preimage ((Complex.imCLM : ℂ →ₗ[ℝ] ℝ))\n\n/-- The half-plane {im z < c} is convex. -/\ntheorem convex_halfplane_im_lt (c : ℝ) : Convex ℝ {z : ℂ | z.im < c} :=\n  (convex_Iio c).linear_preimage ((Complex.imCLM : ℂ →ₗ[ℝ] ℝ))\n\n/-- The level-2 representation on re s > 0: from Zeta23's `Zeta0EqZeta`\nplus the level-2 IBP identity. -/\ntheorem riemannZeta_eq_level2_of_re_pos {s : ℂ} (hs : 0 < s.re) (hs1 : s ≠ 1) :\n    riemannZeta s = 1 / 2 + 1 / (s - 1)\n      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by\n  have hs0 : s ≠ 0 := fun h => by rw [h] at hs; simp at hs\n  have h := Zeta0EqZeta (N := 1) (by norm_num) hs hs1\n  rw [← h]\n  rw [riemannZeta0_apply]\n  have hsum : ∑ n ∈ Finset.range (1 + 1), 1 / (n : ℂ) ^ s = 1 := by\n    rw [Finset.sum_range_succ, Finset.sum_range_one]\n    simp [Complex.zero_cpow hs0]\n  rw [hsum]\n  have hI1 : (∫ x in Set.Ioi ((1 : ℕ) : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1)))\n      = -∫ x in Set.Ioi (1:ℝ), (B1 x : ℂ) * (x : ℂ) ^ (-s - 1) := by\n    rw [← integral_neg]\n    apply integral_congr_ae\n    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n    have hx0 : (0:ℝ) ≤ x := zero_le_one.trans (Set.mem_Ioi.mp hx).le\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  rw [Nat.cast_one, hI1, integral_b1_cpow_eq hs]\n  field_simp\n  ring\n\n/-- The B̃₂ parameter integral is analytic on {re > −1}. -/\ntheorem analyticOnNhd_b2Integral :\n    AnalyticOnNhd ℂ\n      (fun s : ℂ => ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2))\n      {z : ℂ | -1 < z.re} :=\n  (DifferentiableOn.analyticOnNhd\n    (fun z hz => (hasDerivAt_b2Integral hz).differentiableAt.differentiableWithinAt)\n    (isOpen_lt continuous_const Complex.continuous_re))\n\n/-- The level-2 representation on the upper region W⁺ = {re > −1, im > 5}\n(convex, hence preconnected — the identity principle applies). -/\ntheorem riemannZeta_eq_level2_of_im_gt {s : ℂ} (hs : -1 < s.re) (hs5 : 5 < s.im) :\n    riemannZeta s = 1 / 2 + 1 / (s - 1)\n      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by\n  set W : Set ℂ := {z | -1 < z.re ∧ 5 < z.im}\n  have hWopen : IsOpen W :=\n    (isOpen_lt continuous_const Complex.continuous_re).inter\n      (isOpen_lt continuous_const Complex.continuous_im)\n  have hWpre : IsPreconnected W :=\n    ((convex_halfplane_re_gt _).inter (convex_halfplane_im_gt _)).isPreconnected\n  have hf_an : AnalyticOnNhd ℂ riemannZeta W :=\n    (HolomorphicOn_riemannZeta.mono (fun z hz => by\n      show z ≠ 1\n      intro h1\n      have hz2 := hz.2\n      rw [h1, Complex.one_im] at hz2\n      norm_num at hz2)).analyticOnNhd hWopen\n  have hg_an : AnalyticOnNhd ℂ (fun s : ℂ => 1 / 2 + 1 / (s - 1)\n      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) W := by\n    intro z hz\n    apply AnalyticAt.sub _ (analyticOnNhd_b2Integral z hz.1)\n    apply AnalyticAt.add analyticAt_const\n    apply AnalyticAt.div analyticAt_const (analyticAt_id.sub analyticAt_const)\n    intro h\n    have hz1 : z = 1 := by rwa [sub_eq_zero] at h\n    have hz2 := hz.2\n    rw [hz1, Complex.one_im] at hz2\n    norm_num at hz2\n  have hbase : (2 + 10 * Complex.I) ∈ W := by\n    constructor\n    · simp\n    · simp\n  have hV : {z : ℂ | 0 < z.re ∧ z ≠ 1} ∈ 𝓝 (2 + 10 * Complex.I) := by\n    apply (isOpen_lt continuous_const Complex.continuous_re).inter\n      (isOpen_compl_singleton) |>.mem_nhds\n    constructor\n    · simp\n    · simp\n  have hEq : riemannZeta =ᶠ[𝓝 (2 + 10 * Complex.I)] (fun s : ℂ => 1 / 2 + 1 / (s - 1)\n      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) :=\n    hV.eventually_nhds...  -- hmm use filter_upwards [hV]\n  sorry\n  sorry\n\nend NguyenRH1\n\nend"},"extra_content":null}]