LiRBound.lean

Declarations

Source

/-
NguyenRH1/LiRBound.lean — tier ii′ sub-stage ii′-5 (design D-067):
the R-bound for −ζ′/ζ off the near zeros, by the Davenport local route.

§1 (this file's first block, ii′-5b): the second periodic Bernoulli
function B̃₂ and the level-2 Euler–Maclaurin representation

  ζ(s) = 1/2 + 1/(s−1) − s(s+1)·∫₁^∞ B̃₂(x)·x^{−s−2} dx   (re s > −1, s ≠ 1)

giving the polynomial bound ‖ζ(s)‖ ≤ (3/4)|t|² on the disc
B(2+it, 5/2) (σ ≥ −1/2, |t| ≥ 10) — the Γ-free strip bound that the
Davenport disc argument (ii′-5c) consumes. B̃₂(x) = (u²−u)/2 with
u = Int.fract x: continuous (endpoint-matched via `ContinuousOn.comp_fract''`),
1-periodic, values in [−1/8, 0]; HasDerivAt (fract x − 1/2) off ℤ.

Route (D-067 §2): one IBP level over Zeta23's B₁ representation
`Zeta0EqZeta` (riemannZeta0 1 s = riemannZeta s for re s > 0), then the
identity principle across re s = 0. No complex Stirling, no Hadamard.

Archive references: D-067, D-064 §4 R3, journal-022.
-/
import Mathlib
import Zeta23.FromPNTPlus.ZetaBounds
import NguyenRH1.LiContour

open Zeta23 Complex Filter Topology MeasureTheory
open scoped Nat

noncomputable section

namespace NguyenRH1

/-! ## 1. The periodic Bernoulli primitive B̃₂ -/

/-- The second periodic Bernoulli function: B̃₂(x) = (u²−u)/2 with
u = Int.fract x ∈ [0,1). Continuous, 1-periodic, values in [−1/8, 0];
an antiderivative of the sawtooth Int.fract x − 1/2 off the integers. -/
def b2Fun (x : ℝ) : ℝ := (Int.fract x ^ 2 - Int.fract x) / 2

/-- B̃₂ is 1-periodic (global — Int.fract is). -/
theorem b2Fun_add_one (x : ℝ) : b2Fun (x + 1) = b2Fun x := by
  unfold b2Fun
  rw [Int.fract_add_one]

/-- The range of B̃₂: −1/8 ≤ B̃₂(x) ≤ 0 (u(1−u) ∈ [0, 1/4] for u ∈ [0,1)). -/
theorem b2Fun_range (x : ℝ) : -1/8 ≤ b2Fun x ∧ b2Fun x ≤ 0 := by
  have hu0 : 0 ≤ Int.fract x := Int.fract_nonneg x
  have hu1 : Int.fract x < 1 := Int.fract_lt_one x
  unfold b2Fun
  constructor
  · nlinarith [sq_nonneg (Int.fract x - 1/2)]
  · nlinarith

theorem abs_b2Fun_le (x : ℝ) : |b2Fun x| ≤ 1/8 := by
  obtain ⟨h1, h2⟩ := b2Fun_range x
  rw [abs_of_nonpos h2]
  linarith

/-- B̃₂ vanishes at the integers (fract = 0 there). -/
theorem b2Fun_intCast (n : ℤ) : b2Fun (n : ℝ) = 0 := by
  unfold b2Fun
  rw [Int.fract_intCast]
  norm_num

theorem b2Fun_one : b2Fun 1 = 0 := by
  have := b2Fun_intCast 1
  norm_num at this
  exact this

/-- B̃₂ is continuous everywhere: b2Fun = g ∘ Int.fract with
g(u) = (u²−u)/2 on [0,1] satisfying g(0) = g(1). -/
theorem continuous_b2Fun : Continuous b2Fun :=
  ContinuousOn.comp_fract'' (f := fun u : ℝ => (u ^ 2 - u) / 2)
    ((by fun_prop : Continuous (fun u : ℝ => (u ^ 2 - u) / 2)).continuousOn) (by norm_num)

/-- Off the integers, B̃₂ has derivative fract x − 1/2. -/
theorem hasDerivAt_b2Fun {x : ℝ} (hx : Int.fract x ≠ 0) :
    HasDerivAt b2Fun (Int.fract x - 1/2) x := by
  have hIco : Set.Ico (⌊x⌋ : ℝ) (⌊x⌋ + 1) ∈ 𝓝 x := by
    apply Ico_mem_nhds _ (Int.lt_floor_add_one x)
    exact (Int.floor_le x).lt_of_ne (fun h => hx (by rw [Int.fract, h, sub_self]))
  have hEq : (Int.fract : ℝ → ℝ) =ᶠ[𝓝 x] fun y => y - (⌊x⌋ : ℝ) := by
    filter_upwards [hIco] with y hy
    rw [Int.fract, Int.floor_eq_on_Ico _ _ hy]
  have hf : HasDerivAt (Int.fract : ℝ → ℝ) 1 x := by
    have h := (hasDerivAt_id x).sub_const (⌊x⌋ : ℝ)
    exact h.congr_of_eventuallyEq hEq
  unfold b2Fun
  refine (((hf.pow 2).sub hf).div_const 2).congr_deriv ?_
  ring

/-! ## 2. The level-2 Euler–Maclaurin identity -/

/-- Zeta23's sawtooth `B1` equals Int.fract − 1/2 on [0, ∞). -/
theorem b1_eq_fract_sub_half {x : ℝ} (hx : 0 ≤ x) : B1 x = Int.fract x - 1 / 2 := by
  unfold B1 Int.fract
  rw [natCast_floor_eq_intCast_floor hx]

/-- The unit-interval IBP: over each integer interval [k, k+1] (k ≥ 1),
∫ B̃₁·x^{−s−1} = (s+1)·∫ B̃₂·x^{−s−2} (boundary terms vanish: B̃₂ = 0 at
the integers). -/
theorem intervalIntegral_b1_cpow (k : ℕ) (hk : 1 ≤ k) (s : ℂ) (hs : s ≠ -1) :
    ∫ x in (k : ℝ)..(k + 1 : ℝ), (B1 x : ℂ) * (x : ℂ) ^ (-s - 1)
      = (s + 1) * ∫ x in (k : ℝ)..(k + 1 : ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by
  have hk0 : (0:ℝ) < (k : ℝ) := by exact_mod_cast hk
  have hr : (-s - 1) ≠ 0 := by
    intro h
    exact hs (neg_eq_iff_eq_neg.mp (sub_eq_zero.mp h))
  have hu : ContinuousOn (fun x : ℝ => (b2Fun x : ℂ)) (Set.uIcc (k : ℝ) (k + 1 : ℝ)) :=
    (continuous_ofReal.comp continuous_b2Fun).continuousOn
  have hv : ContinuousOn (fun x : ℝ => (x : ℂ) ^ (-s - 1)) (Set.uIcc (k : ℝ) (k + 1 : ℝ)) := by
    rw [Set.uIcc_of_le (by linarith : (k:ℝ) ≤ k + 1)]
    intro x hx
    have hx0 : x ≠ 0 := by linarith [hx.1]
    exact (continuousAt_ofReal_cpow_const x _ (Or.inr hx0)).continuousWithinAt
  have hIco_x : ∀ x ∈ Set.Ioo (k : ℝ) (k + 1 : ℝ), x ∈ Set.Ico (⌊x⌋ : ℝ) (⌊x⌋ + 1) :=
    fun x _ => ⟨Int.floor_le x, Int.lt_floor_add_one x⟩
  have huu' : ∀ x ∈ Set.Ioo (min (k : ℝ) (k + 1 : ℝ)) (max (k : ℝ) (k + 1 : ℝ)),
      HasDerivAt (fun x : ℝ => (b2Fun x : ℂ)) ((B1 x : ℂ)) x := by
    intro x hx
    rw [min_eq_left (by linarith : (k:ℝ) ≤ k + 1), max_eq_right (by linarith : (k:ℝ) ≤ k + 1)] at hx
    have hfr : Int.fract x ≠ 0 := by
      intro h
      rw [Int.fract] at h
      have hxeq : x = ⌊x⌋ := sub_eq_zero.mp h
      have hxk : ⌊x⌋ = (k : ℤ) := by
        apply Int.floor_eq_on_Ico
        refine ⟨?_, ?_⟩
        · have h1 : ((k : ℤ) : ℝ) ≤ x := by push_cast; linarith [hx.1.le]
          exact h1
        · have h2 : x < ((k : ℤ) : ℝ) + 1 := by push_cast; linarith [hx.2]
          exact h2
      rw [hxk] at hxeq
      have hlt : (k : ℝ) < x := hx.1
      rw [hxeq] at hlt
      norm_num at hlt
    have hb := (hasDerivAt_b2Fun hfr).ofReal_comp
    rw [← b1_eq_fract_sub_half (by linarith [hx.1] : (0:ℝ) ≤ x)] at hb
    exact hb
  have hvv' : ∀ x ∈ Set.Ioo (min (k : ℝ) (k + 1 : ℝ)) (max (k : ℝ) (k + 1 : ℝ)),
      HasDerivAt (fun x : ℝ => (x : ℂ) ^ (-s - 1)) ((-(s + 1)) * (x : ℂ) ^ (-s - 2)) x := by
    intro x hx
    rw [min_eq_left (by linarith : (k:ℝ) ≤ k + 1), max_eq_right (by linarith : (k:ℝ) ≤ k + 1)] at hx
    have hx0 : x ≠ 0 := by linarith [hx.1]
    have h := hasDerivAt_ofReal_cpow_const hx0 hr
    refine h.congr_deriv ?_
    rw [show -s - 1 - 1 = -s - 2 by ring]
    ring
  have hu'int : IntervalIntegrable (fun x : ℝ => (B1 x : ℂ)) volume (k : ℝ) (k + 1 : ℝ) := by
    rw [intervalIntegrable_iff']
    apply MeasureTheory.Measure.integrableOn_of_bounded (by simp)
      (by fun_prop) (M := 1 / 2)
    filter_upwards [self_mem_ae_restrict (by measurability)] with x hx
    rw [Set.uIcc_of_le (by linarith : (k : ℝ) ≤ k + 1)] at hx
    rw [Complex.norm_real]
    exact abs_B1_le_half (by linarith [hx.1])
  have hv'int : IntervalIntegrable
      (fun x : ℝ => (-(s + 1)) * (x : ℂ) ^ (-s - 2)) volume (k : ℝ) (k + 1 : ℝ) := by
    apply IntervalIntegrable.const_mul
    apply ContinuousOn.intervalIntegrable
    rw [Set.uIcc_of_le (by linarith : (k:ℝ) ≤ k + 1)]
    intro x hx
    have hx0 : x ≠ 0 := by linarith [hx.1]
    exact (continuousAt_ofReal_cpow_const x _ (Or.inr hx0)).continuousWithinAt
  -- the IBP itself
  have hIBP := intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivAt
    (u := fun x : ℝ => (b2Fun x : ℂ)) (u' := fun x : ℝ => (B1 x : ℂ))
    (v := fun x : ℝ => (x : ℂ) ^ (-s - 1)) (v' := fun x : ℝ => (-(s + 1)) * (x : ℂ) ^ (-s - 2))
    hu hv huu' hvv' hu'int hv'int
  -- boundary terms vanish (b2Fun = 0 at k and k+1)
  have hb1 : b2Fun (k : ℝ) = 0 := by
    have : (k : ℝ) = ((k : ℤ) : ℝ) := by simp
    rw [this]
    exact b2Fun_intCast k
  have hb2 : b2Fun ((k : ℝ) + 1) = 0 := by
    have : (k : ℝ) + 1 = ((k + 1 : ℤ) : ℝ) := by push_cast; ring
    rw [this]
    exact b2Fun_intCast (k + 1)
  rw [hb1, hb2] at hIBP
  simp only [Complex.ofReal_zero, zero_mul, sub_self, zero_sub] at hIBP
  -- hIBP : ∫ u*v' = −∫ u'*v; rearrange
  rw [show (fun x : ℝ => (b2Fun x : ℂ) * ((-(s + 1)) * (x : ℂ) ^ (-s - 2)))
      = fun x : ℝ => (-(s + 1)) * ((b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) from
    funext fun x => by ring] at hIBP
  rw [intervalIntegral.integral_const_mul] at hIBP
  rw [neg_mul] at hIBP
  exact (neg_inj.mp hIBP).symm

/-- B̃₁ is interval-integrable on any interval in [0, ∞). -/
theorem intervalIntegrable_b1 {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) :
    IntervalIntegrable (fun x : ℝ => (B1 x : ℂ)) volume a b := by
  rw [intervalIntegrable_iff', Set.uIcc_of_le hab]
  apply MeasureTheory.Measure.integrableOn_of_bounded (by simp) (by fun_prop) (M := 1 / 2)
  filter_upwards [self_mem_ae_restrict (by measurability)] with x hx
  rw [Complex.norm_real]
  exact abs_B1_le_half (by linarith [hx.1])

/-- The ofReal-cpow is interval-integrable on intervals in (0, ∞). -/
theorem intervalIntegrable_cpow (c : ℂ) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
    IntervalIntegrable (fun x : ℝ => (x : ℂ) ^ c) volume a b := by
  apply ContinuousOn.intervalIntegrable
  rw [Set.uIcc_of_le hab]
  intro x hx
  exact (continuousAt_ofReal_cpow_const x _ (Or.inr (by linarith [hx.1]))).continuousWithinAt

/-- Product integrability: B̃₁·x^c on intervals in (0, ∞). -/
theorem intervalIntegrable_b1_mul_cpow (c : ℂ) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
    IntervalIntegrable (fun x : ℝ => (B1 x : ℂ) * (x : ℂ) ^ c) volume a b := by
  apply (intervalIntegrable_b1 ha.le hab).mul_continuousOn
  rw [Set.uIcc_of_le hab]
  intro x hx
  exact (continuousAt_ofReal_cpow_const x _ (Or.inr (by linarith [hx.1]))).continuousWithinAt

/-- Product integrability: B̃₂·x^c on intervals in (0, ∞). -/
theorem intervalIntegrable_b2_mul_cpow (c : ℂ) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
    IntervalIntegrable (fun x : ℝ => (b2Fun x : ℂ) * (x : ℂ) ^ c) volume a b := by
  apply IntervalIntegrable.mul_continuousOn
  · exact (continuous_ofReal.comp continuous_b2Fun).continuousOn.intervalIntegrable
  · rw [Set.uIcc_of_le hab]
    intro x hx
    exact (continuousAt_ofReal_cpow_const x _ (Or.inr (by linarith [hx.1]))).continuousWithinAt

/-- The IBP identity summed to [1, N] (natural N ≥ 1). -/
theorem intervalIntegral_b1_cpow_nat (N : ℕ) (hN : 1 ≤ N) (s : ℂ) (hs : s ≠ -1) :
    ∫ x in (1:ℝ)..(N : ℝ), (B1 x : ℂ) * (x : ℂ) ^ (-s - 1)
      = (s + 1) * ∫ x in (1:ℝ)..(N : ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by
  induction N with
  | zero => exact absurd hN (by norm_num)
  | succ N ih =>
    rcases Nat.eq_zero_or_pos N with hN0 | hNpos
    · subst hN0
      simp
    · have hsucc : ((N + 1 : ℕ) : ℝ) = (N : ℝ) + 1 := by push_cast; ring
      rw [hsucc]
      have hN1 : (1:ℝ) ≤ (N : ℝ) := by exact_mod_cast hNpos
      have hNN : (N : ℝ) ≤ (N : ℝ) + 1 := by linarith
      have hN0R : (0:ℝ) < (N : ℝ) := by exact_mod_cast hNpos
      rw [← intervalIntegral.integral_add_adjacent_intervals
        (intervalIntegrable_b1_mul_cpow (-s - 1) one_pos hN1)
        (intervalIntegrable_b1_mul_cpow (-s - 1) hN0R hNN)]
      rw [ih hNpos, intervalIntegral_b1_cpow N hNpos s hs]
      rw [← intervalIntegral.integral_add_adjacent_intervals
        (intervalIntegrable_b2_mul_cpow (-s - 2) one_pos hN1)
        (intervalIntegrable_b2_mul_cpow (-s - 2) hN0R hNN)]
      ring

/-- The B̃₂·x^{−s−2} integrand is integrable on (1, ∞) for re s > −1. -/
theorem integrableOn_b2_cpow {s : ℂ} (hs : -1 < s.re) :
    IntegrableOn (fun x : ℝ => (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) (Set.Ioi 1) := by
  have hg : IntegrableOn (fun x : ℝ => x ^ (-s.re - 2)) (Set.Ioi 1) :=
    integrableOn_Ioi_rpow_of_lt (show -s.re - 2 < -1 by linarith) one_pos
  have hmeas : AEStronglyMeasurable (fun x : ℝ => (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2))
      (volume.restrict (Set.Ioi (1:ℝ))) := by
    apply ContinuousOn.aestronglyMeasurable _ measurableSet_Ioi
    apply ContinuousOn.mul
    · exact (continuous_ofReal.comp continuous_b2Fun).continuousOn
    · intro x hx
      exact (continuousAt_ofReal_cpow_const x _
        (Or.inr (by linarith [Set.mem_Ioi.mp hx] : x ≠ 0))).continuousWithinAt
  have hbound : ∀ᵐ x ∂(volume.restrict (Set.Ioi 1)),
      ‖(b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖ ≤ x ^ (-s.re - 2) := by
    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx
    have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx
    have hnorm : ‖(x : ℂ) ^ (-s - 2)‖ = x ^ (-s.re - 2) := by
      rw [norm_cpow_eq_rpow_re_of_pos (by linarith)]
      congr 2
    rw [norm_mul, Complex.norm_real, hnorm]
    calc |b2Fun x| * x ^ (-s.re - 2)
        ≤ (1 / 8) * x ^ (-s.re - 2) :=
          mul_le_mul_of_nonneg_right (abs_b2Fun_le x) (Real.rpow_nonneg (by linarith) _)
      _ ≤ x ^ (-s.re - 2) :=
          mul_le_of_le_one_left (Real.rpow_nonneg (by linarith) _) (by norm_num)
  exact Integrable.mono' hg hmeas hbound

/-- The log-weighted B̃₂ integrand is integrable on (1, ∞) for re s > −1. -/
theorem integrableOn_b2_cpow_log {s : ℂ} (hs : -1 < s.re) :
    IntegrableOn (fun x : ℝ => (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) * (-Real.log x)))
      (Set.Ioi 1) := by
  have hg : IntegrableOn (fun x : ℝ => x ^ (-s.re - 2) * |Real.log x|) (Set.Ioi 1) := by
    have h := integrable_log_over_pow (r := -s.re - 1) (by linarith) (N := 1) (by norm_num)
    rw [Nat.cast_one] at h
    refine h.congr_fun ?_ measurableSet_Ioi
    intro x hx
    have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx
    show ‖x ^ (-s.re - 1 - 1)‖ * ‖Real.log x‖ = x ^ (-s.re - 2) * |Real.log x|
    have h1 : ‖x ^ (-s.re - 1 - 1)‖ = x ^ (-s.re - 2) := by
      rw [Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _)]
      congr 1
      ring
    rw [h1, Real.norm_eq_abs, abs_of_nonneg (Real.log_nonneg hx1.le)]
  have hmeas : AEStronglyMeasurable (fun x : ℝ => (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) *
      (-Real.log x))) (volume.restrict (Set.Ioi (1:ℝ))) := by
    apply ContinuousOn.aestronglyMeasurable _ measurableSet_Ioi
    apply ContinuousOn.mul
    · exact (continuous_ofReal.comp continuous_b2Fun).continuousOn
    · apply ContinuousOn.mul
      · intro x hx
        exact (continuousAt_ofReal_cpow_const x _
          (Or.inr (by linarith [Set.mem_Ioi.mp hx] : x ≠ 0))).continuousWithinAt
      · have hlog : ContinuousOn (fun x : ℝ => (Real.log x : ℂ)) (Set.Ioi (1:ℝ)) :=
          continuous_ofReal.comp_continuousOn (Real.continuousOn_log.mono
            (fun x hx => Set.mem_compl_singleton_iff.mpr (by linarith [Set.mem_Ioi.mp hx])))
        exact hlog.neg
  have hbound : ∀ᵐ x ∂(volume.restrict (Set.Ioi 1)),
      ‖(b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) * (-Real.log x))‖ ≤ x ^ (-s.re - 2) * |Real.log x| := by
    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx
    have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx
    have hnorm : ‖(x : ℂ) ^ (-s - 2)‖ = x ^ (-s.re - 2) := by
      rw [norm_cpow_eq_rpow_re_of_pos (by linarith)]
      congr 2
    rw [norm_mul, norm_mul, Complex.norm_real, hnorm]
    rw [show ‖(-(Real.log x : ℝ) : ℂ)‖ = |Real.log x| by
      rw [norm_neg, Complex.norm_real, Real.norm_eq_abs]]
    calc |b2Fun x| * (x ^ (-s.re - 2) * |Real.log x|)
        ≤ (1 / 8) * (x ^ (-s.re - 2) * |Real.log x|) :=
          mul_le_mul_of_nonneg_right (abs_b2Fun_le x)
            (mul_nonneg (Real.rpow_nonneg (by linarith) _) (abs_nonneg _))
      _ ≤ x ^ (-s.re - 2) * |Real.log x| :=
          mul_le_of_le_one_left (mul_nonneg (Real.rpow_nonneg (by linarith) _) (abs_nonneg _))
            (by norm_num)
  exact Integrable.mono' hg hmeas hbound

/-- **The level-2 Euler–Maclaurin identity** (re s > 0):
∫₁^∞ B̃₁·x^{−s−1} = (s+1)·∫₁^∞ B̃₂·x^{−s−2}. -/
theorem integral_b1_cpow_eq {s : ℂ} (hs : 0 < s.re) :
    ∫ x in Set.Ioi (1:ℝ), (B1 x : ℂ) * (x : ℂ) ^ (-s - 1)
      = (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by
  have hInt1 : IntegrableOn (fun x : ℝ => (B1 x : ℂ) * (x : ℂ) ^ (-s - 1)) (Set.Ioi 1) := by
    have h := (integrableOn_of_Zeta0_fun (N := 1) (by norm_num) (s := s) hs).neg
    rw [Nat.cast_one] at h
    apply IntegrableOn.congr_fun h _ measurableSet_Ioi
    intro x hx
    have hx0 : (0:ℝ) ≤ x := zero_le_one.trans (Set.mem_Ioi.mp hx).le
    simp only [Pi.neg_apply]
    rw [b1_eq_fract_sub_half hx0, Int.fract]
    have e : (-(s + 1) : ℂ) = -s - 1 := by ring
    rw [e]
    push_cast
    ring
  have hT1 := intervalIntegral_tendsto_integral_Ioi (a := (1:ℝ)) (b := fun N : ℕ => (N : ℝ))
    hInt1 tendsto_natCast_atTop_atTop
  have hT2 := intervalIntegral_tendsto_integral_Ioi (a := (1:ℝ)) (b := fun N : ℕ => (N : ℝ))
    (integrableOn_b2_cpow (by linarith)) tendsto_natCast_atTop_atTop
  have heq : ∀ᶠ N : ℕ in atTop,
      (∫ x in (1:ℝ)..(N : ℝ), (B1 x : ℂ) * (x : ℂ) ^ (-s - 1))
        = (s + 1) * ∫ x in (1:ℝ)..(N : ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by
    filter_upwards [Filter.eventually_atTop.mpr ⟨1, fun N hN =>
      intervalIntegral_b1_cpow_nat N hN s (fun h => by
        have : s.re = -1 := by rw [h]; simp
        linarith)⟩] with N hN
    exact hN
  exact tendsto_nhds_unique (hT1.congr' heq) (hT2.const_mul (s + 1))

/-! ## 3. Analyticity of the B̃₂ parameter integral -/

/-- The B̃₂ parameter integral is differentiable on re s > −1, with the
log-weighted derivative. (Clone of Zeta23's `hasDerivAt_Zeta0Integral`
with one more power of decay, per D-067 §2.) -/
theorem hasDerivAt_b2Integral {s : ℂ} (hs : -1 < s.re) :
    HasDerivAt (fun z : ℂ => ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-z - 2))
      (∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) * (-Real.log x))) s := by
  set f : ℝ → ℂ := fun x ↦ (b2Fun x : ℂ)
  set F : ℂ → ℝ → ℂ := fun z x ↦ (x : ℂ) ^ (-z - 2) * f x
  set F' : ℂ → ℝ → ℂ := fun z x ↦ (x : ℂ) ^ (-z - 2) * (-Real.log x) * f x
  set ε := (s.re + 1) / 2
  have hε_def : ε = (s.re + 1) / 2 := rfl
  have ε_pos : 0 < ε := by rw [hε_def]; linarith
  set bound : ℝ → ℝ := fun x ↦ |x ^ (-(s.re + 3) / 2)| * |Real.log x|
  let μ : Measure ℝ := volume.restrict (Set.Ioi (1:ℝ))
  have hF_meas : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) μ := by
    have hU : {z : ℂ | -1 < z.re} ∈ 𝓝 s := by
      rw [mem_nhds_iff]
      exact ⟨{z | -1 < z.re}, fun _ a ↦ a, isOpen_lt continuous_const Complex.continuous_re, hs⟩
    filter_upwards [hU] with z hz
    have h := (integrableOn_b2_cpow hz).aestronglyMeasurable
    exact h.congr (Filter.Eventually.of_forall fun x => by simp only [F, f]; ring)
  have hF_int : Integrable (F s) μ := by
    apply Integrable.congr (integrableOn_b2_cpow hs)
    filter_upwards with x
    simp only [F, f]
    ring
  have hF'_meas : AEStronglyMeasurable (F' s) μ := by
    have h := (integrableOn_b2_cpow_log hs).aestronglyMeasurable
    exact h.congr (Filter.Eventually.of_forall fun x => by simp only [F', f]; ring)
  have h_bound : ∀ᵐ x ∂μ, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x := by
    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx
    have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx
    intro z hz
    have hzre : (s.re - 1) / 2 < z.re := by
      rw [Metric.mem_ball, Complex.dist_eq] at hz
      have h1 : |z.re - s.re| ≤ ‖z - s‖ := abs_re_le_norm (z - s)
      have h2 : z.re - s.re > -ε := by
        have h3 : |z.re - s.re| < ε := lt_of_le_of_lt h1 hz
        linarith [abs_lt.mp h3]
      rw [hε_def] at h2
      linarith [h2]
    have hpow : ‖(x : ℂ) ^ (-z - 2)‖ ≤ x ^ (-(s.re + 3) / 2) := by
      rw [norm_cpow_eq_rpow_re_of_pos (by linarith)]
      have h3 : (-z - 2).re = -z.re - 2 := by simp
      rw [h3]
      apply Real.rpow_le_rpow_of_exponent_le (by linarith)
      linarith [hzre]
    calc ‖F' z x‖ = ‖(x : ℂ) ^ (-z - 2)‖ * |Real.log x| * |b2Fun x| := by
            simp only [F', f, norm_mul, norm_neg, Complex.norm_real, Real.norm_eq_abs]
      _ ≤ x ^ (-(s.re + 3) / 2) * |Real.log x| * (1 / 8) := by
            have h1 : ‖(x : ℂ) ^ (-z - 2)‖ * |Real.log x|
                ≤ x ^ (-(s.re + 3) / 2) * |Real.log x| :=
              mul_le_mul_of_nonneg_right hpow (abs_nonneg _)
            calc ‖(x : ℂ) ^ (-z - 2)‖ * |Real.log x| * |b2Fun x|
                ≤ (x ^ (-(s.re + 3) / 2) * |Real.log x|) * |b2Fun x| :=
                  mul_le_mul_of_nonneg_right h1 (abs_nonneg _)
              _ ≤ (x ^ (-(s.re + 3) / 2) * |Real.log x|) * (1 / 8) :=
                  mul_le_mul_of_nonneg_left (abs_b2Fun_le x)
                    (mul_nonneg (Real.rpow_nonneg (by linarith) _) (abs_nonneg _))
      _ ≤ x ^ (-(s.re + 3) / 2) * |Real.log x| * 1 :=
            mul_le_mul_of_nonneg_left (by norm_num : (1/8 : ℝ) ≤ 1)
              (mul_nonneg (Real.rpow_nonneg (by linarith) _) (abs_nonneg _))
      _ = bound x := by
            simp only [bound, mul_one]
            rw [Real.abs_rpow_of_nonneg (by linarith), abs_of_pos (by linarith : (0:ℝ) < x)]
  have bound_integrable : Integrable bound μ := by
    have h := integrable_log_over_pow (r := -(s.re + 1) / 2) (by linarith) (N := 1) (by norm_num)
    rw [Nat.cast_one] at h
    refine h.congr_fun ?_ measurableSet_Ioi
    intro x hx
    have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx
    show ‖x ^ (-(s.re + 1) / 2 - 1)‖ * ‖Real.log x‖ = |x ^ (-(s.re + 3) / 2)| * |Real.log x|
    rw [Real.norm_eq_abs, Real.norm_eq_abs, Real.abs_rpow_of_nonneg (by linarith),
      Real.abs_rpow_of_nonneg (by linarith)]
    congr 2
    ring
  have h_diff : ∀ᵐ x ∂μ, ∀ z ∈ Metric.ball s ε, HasDerivAt (fun w ↦ F w x) (F' z x) z := by
    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx
    have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx
    intro z hz
    have h1 : HasDerivAt (fun w : ℂ => (x : ℂ) ^ (-w - 2))
        ((x : ℂ) ^ (-z - 2) * Complex.log (x : ℂ) * (-1)) z :=
      HasDerivAt.const_cpow (c := (x : ℂ)) (f := fun w : ℂ => -w - 2) (f' := -1) (x := z)
        ((hasDerivAt_id z).neg.sub_const 2)
        (Or.inl (Complex.ofReal_ne_zero.mpr (by linarith)))
    have h2 := h1.mul_const (f x)
    have hfun : (fun w ↦ F w x) = (fun y ↦ (x : ℂ) ^ (-y - 2) * f x) := by
      ext w
      simp only [F]
    have hval : F' z x = (x : ℂ) ^ (-z - 2) * Complex.log (x : ℂ) * (-1) * f x := by
      simp only [F', f]
      rw [Complex.ofReal_log (by linarith : (0:ℝ) ≤ x)]
      ring
    rw [hfun, hval]
    exact h2
  have key := (hasDerivAt_integral_of_dominated_loc_of_deriv_le (F := F) (F' := F') (x₀ := s)
    (s := Metric.ball s ε) (bound := bound) (μ := μ) (Metric.ball_mem_nhds s ε_pos)
    hF_meas hF_int hF'_meas h_bound bound_integrable h_diff).2
  have keyI : HasDerivAt (fun z : ℂ => ∫ x in Set.Ioi (1:ℝ), F z x)
      (∫ x in Set.Ioi (1:ℝ), F' s x) s := key
  convert keyI using 1
  · ext z
    apply integral_congr_ae
    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx
    simp only [F, f]
    ring
  · apply integral_congr_ae
    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx
    simp only [F', f]
    ring

/-! ## 4. The level-2 representation of ζ on re s > −1 -/

/-- The half-plane {c < re z} is convex. -/
theorem convex_halfplane_re_gt (c : ℝ) : Convex ℝ {z : ℂ | c < z.re} :=
  (convex_Ioi c).linear_preimage ((Complex.reCLM : ℂ →ₗ[ℝ] ℝ))

/-- The half-plane {c < im z} is convex. -/
theorem convex_halfplane_im_gt (c : ℝ) : Convex ℝ {z : ℂ | c < z.im} :=
  (convex_Ioi c).linear_preimage ((Complex.imCLM : ℂ →ₗ[ℝ] ℝ))

/-- The half-plane {im z < c} is convex. -/
theorem convex_halfplane_im_lt (c : ℝ) : Convex ℝ {z : ℂ | z.im < c} :=
  (convex_Iio c).linear_preimage ((Complex.imCLM : ℂ →ₗ[ℝ] ℝ))

/-- The level-2 representation on re s > 0: from Zeta23's `Zeta0EqZeta`
plus the level-2 IBP identity. -/
theorem riemannZeta_eq_level2_of_re_pos {s : ℂ} (hs : 0 < s.re) (hs1 : s ≠ 1) :
    riemannZeta s = 1 / 2 + 1 / (s - 1)
      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by
  have hs0 : s ≠ 0 := fun h => by rw [h] at hs; simp at hs
  have h := Zeta0EqZeta (N := 1) (by norm_num) hs hs1
  rw [← h]
  rw [riemannZeta0_apply]
  have hsum : ∑ n ∈ Finset.range (1 + 1), 1 / (n : ℂ) ^ s = 1 := by
    rw [Finset.sum_range_succ, Finset.sum_range_one]
    simp [Complex.zero_cpow hs0]
  rw [hsum]
  have hI1 : (∫ x in Set.Ioi (1:ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1)))
      = -∫ x in Set.Ioi (1:ℝ), (B1 x : ℂ) * (x : ℂ) ^ (-s - 1) := by
    rw [← integral_neg]
    apply integral_congr_ae
    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx
    have hx0 : (0:ℝ) ≤ x := zero_le_one.trans (Set.mem_Ioi.mp hx).le
    rw [b1_eq_fract_sub_half hx0, Int.fract]
    have e : (-(s + 1) : ℂ) = -s - 1 := by ring
    rw [e]
    push_cast
    ring
  simp only [Nat.cast_one]
  rw [hI1, integral_b1_cpow_eq hs]
  have e1 : (-(1 : ℂ) ^ (1 - s)) / (1 - s) = 1 / (s - 1) := by
    rw [Complex.one_cpow]
    field_simp [sub_ne_zero.mpr hs1]
    ring
  have e2 : (-(1 : ℂ) ^ (-s)) / 2 = -1 / 2 := by
    rw [Complex.one_cpow]
  rw [e1, e2]
  ring

/-- The B̃₂ parameter integral is analytic on {re > −1}. -/
theorem analyticOnNhd_b2Integral :
    AnalyticOnNhd ℂ
      (fun s : ℂ => ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2))
      {z : ℂ | -1 < z.re} :=
  (DifferentiableOn.analyticOnNhd
    (fun _z hz => (hasDerivAt_b2Integral hz).differentiableAt.differentiableWithinAt)
    (isOpen_lt continuous_const Complex.continuous_re))

/-- The level-2 representation on the upper region W⁺ = {re > −1, im > 5}
(convex, hence preconnected — the identity principle applies). -/
theorem riemannZeta_eq_level2_of_im_gt {s : ℂ} (hs : -1 < s.re) (hs5 : 5 < s.im) :
    riemannZeta s = 1 / 2 + 1 / (s - 1)
      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by
  set W : Set ℂ := {z | -1 < z.re ∧ 5 < z.im}
  have hWopen : IsOpen W :=
    (isOpen_lt continuous_const Complex.continuous_re).inter
      (isOpen_lt continuous_const Complex.continuous_im)
  have hWpre : IsPreconnected W :=
    ((convex_halfplane_re_gt _).inter (convex_halfplane_im_gt _)).isPreconnected
  have hf_an : AnalyticOnNhd ℂ riemannZeta W :=
    (HolomorphicOn_riemannZeta.mono (fun z hz => by
      show z ≠ 1
      intro h1
      have hz2 := hz.2
      rw [h1, Complex.one_im] at hz2
      norm_num at hz2)).analyticOnNhd hWopen
  have hg_an : AnalyticOnNhd ℂ (fun s : ℂ => 1 / 2 + 1 / (s - 1)
      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) W := by
    intro z hz
    apply AnalyticAt.sub
    · apply AnalyticAt.add analyticAt_const
      apply AnalyticAt.div analyticAt_const (analyticAt_id.sub analyticAt_const)
      intro h
      simp only [Pi.sub_apply, id_eq] at h
      have hz1 : z = 1 := sub_eq_zero.mp h
      have hz2 := hz.2
      rw [hz1, Complex.one_im] at hz2
      norm_num at hz2
    · apply AnalyticAt.mul
      · exact analyticAt_id.mul (analyticAt_id.add analyticAt_const)
      · exact analyticOnNhd_b2Integral z hz.1
  have hbase : (2 + 10 * Complex.I) ∈ W := by
    refine ⟨by simp; try norm_num, by simp; try norm_num⟩
  have hV : {z : ℂ | 0 < z.re ∧ z ≠ 1} ∈ 𝓝 (2 + 10 * Complex.I) := by
    apply ((isOpen_lt continuous_const Complex.continuous_re).inter
      isOpen_compl_singleton).mem_nhds
    refine ⟨by simp; try norm_num, by norm_num [Complex.ext_iff]⟩
  have hEq : riemannZeta =ᶠ[𝓝 (2 + 10 * Complex.I)] (fun s : ℂ => 1 / 2 + 1 / (s - 1)
      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) := by
    filter_upwards [hV] with z hz
    exact riemannZeta_eq_level2_of_re_pos hz.1 hz.2
  have hOn := hf_an.eqOn_of_preconnected_of_eventuallyEq hg_an hWpre hbase hEq
  exact hOn ⟨hs, hs5⟩

/-- The level-2 representation on the lower region W⁻ = {re > −1, im < −5}. -/
theorem riemannZeta_eq_level2_of_im_lt {s : ℂ} (hs : -1 < s.re) (hs5 : s.im < -5) :
    riemannZeta s = 1 / 2 + 1 / (s - 1)
      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by
  set W : Set ℂ := {z | -1 < z.re ∧ z.im < -5}
  have hWopen : IsOpen W :=
    (isOpen_lt continuous_const Complex.continuous_re).inter
      (isOpen_lt Complex.continuous_im continuous_const)
  have hWpre : IsPreconnected W :=
    ((convex_halfplane_re_gt _).inter (convex_halfplane_im_lt _)).isPreconnected
  have hf_an : AnalyticOnNhd ℂ riemannZeta W :=
    (HolomorphicOn_riemannZeta.mono (fun z hz => by
      show z ≠ 1
      intro h1
      have hz2 := hz.2
      rw [h1, Complex.one_im] at hz2
      norm_num at hz2)).analyticOnNhd hWopen
  have hg_an : AnalyticOnNhd ℂ (fun s : ℂ => 1 / 2 + 1 / (s - 1)
      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) W := by
    intro z hz
    apply AnalyticAt.sub
    · apply AnalyticAt.add analyticAt_const
      apply AnalyticAt.div analyticAt_const (analyticAt_id.sub analyticAt_const)
      intro h
      simp only [Pi.sub_apply, id_eq] at h
      have hz1 : z = 1 := sub_eq_zero.mp h
      have hz2 := hz.2
      rw [hz1, Complex.one_im] at hz2
      norm_num at hz2
    · apply AnalyticAt.mul
      · exact analyticAt_id.mul (analyticAt_id.add analyticAt_const)
      · exact analyticOnNhd_b2Integral z hz.1
  have hbase : (2 - 10 * Complex.I) ∈ W := by
    refine ⟨by simp; try norm_num, by simp; try norm_num⟩
  have hV : {z : ℂ | 0 < z.re ∧ z ≠ 1} ∈ 𝓝 (2 - 10 * Complex.I) := by
    apply ((isOpen_lt continuous_const Complex.continuous_re).inter
      isOpen_compl_singleton).mem_nhds
    refine ⟨by simp; try norm_num, by norm_num [Complex.ext_iff]⟩
  have hEq : riemannZeta =ᶠ[𝓝 (2 - 10 * Complex.I)] (fun s : ℂ => 1 / 2 + 1 / (s - 1)
      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)) := by
    filter_upwards [hV] with z hz
    exact riemannZeta_eq_level2_of_re_pos hz.1 hz.2
  have hOn := hf_an.eqOn_of_preconnected_of_eventuallyEq hg_an hWpre hbase hEq
  exact hOn ⟨hs, hs5⟩

/-! ## 5. The polynomial bound on the disc B(2+it, 5/2) -/

/-- The B̃₂-integral norm bound: ‖∫₁^∞ B̃₂·x^{−s−2}‖ ≤ (1/8)/(re s + 1)
for re s > −1. -/
theorem norm_b2Integral_le {s : ℂ} (hs : -1 < s.re) :
    ‖∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖
      ≤ (1 / 8) / (s.re + 1) := by
  have h1 : ‖∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖
      ≤ ∫ x in Set.Ioi (1:ℝ), ‖(b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖ :=
    norm_integral_le_integral_norm _
  have hnorm_int : IntegrableOn (fun x : ℝ => ‖(b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖)
      (Set.Ioi 1) :=
    (integrableOn_b2_cpow hs).norm
  have h2 : (∫ x in Set.Ioi (1:ℝ), ‖(b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖)
      ≤ ∫ x in Set.Ioi (1:ℝ), (1 / 8) * x ^ (-s.re - 2) := by
    apply integral_mono_ae hnorm_int
      ((integrableOn_Ioi_rpow_of_lt (show -s.re - 2 < -1 by linarith) one_pos).const_mul _)
    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx
    have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx
    have hnorm : ‖(x : ℂ) ^ (-s - 2)‖ = x ^ (-s.re - 2) := by
      rw [norm_cpow_eq_rpow_re_of_pos (by linarith)]
      congr 2
    rw [norm_mul, Complex.norm_real, hnorm]
    calc |b2Fun x| * x ^ (-s.re - 2)
        ≤ (1 / 8) * x ^ (-s.re - 2) :=
          mul_le_mul_of_nonneg_right (abs_b2Fun_le x) (Real.rpow_nonneg (by linarith) _)
      _ = (1 / 8) * x ^ (-s.re - 2) := rfl
  have h3 : (∫ x in Set.Ioi (1:ℝ), (1 / 8) * x ^ (-s.re - 2)) = (1 / 8) / (s.re + 1) := by
    rw [integral_const_mul, integral_Ioi_rpow_of_lt
      (show -s.re - 2 < -1 by linarith) (one_pos), Real.one_rpow]
    field_simp [(by linarith : s.re + 1 ≠ 0), (by linarith : -s.re - 2 + 1 ≠ 0)]
    ring
  exact h1.trans (h2.trans h3.le)

/-- **The disc bound** (D-067 §2): on B(2+it, 5/2) with |t| ≥ 10,
‖ζ(s)‖ ≤ (3/4)·|t|². -/
theorem norm_riemannZeta_le_disc {t : ℝ} (ht : 10 ≤ |t|) {s : ℂ}
    (hs : s ∈ Metric.closedBall ((2 : ℂ) + t * Complex.I) (5 / 2)) :
    ‖riemannZeta s‖ ≤ 3 / 4 * |t| ^ 2 := by
  have hdist : ‖s - (2 + t * Complex.I)‖ ≤ 5 / 2 := by
    rw [Metric.mem_closedBall, Complex.dist_eq] at hs
    exact hs
  have hresub : (s - (2 + t * Complex.I)).re = s.re - 2 := by
    simp [sub_re, mul_re, ofReal_re, ofReal_im, I_re, I_im]
  have himsub : (s - (2 + t * Complex.I)).im = s.im - t := by
    simp [sub_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]
  have hre : -1 / 2 ≤ s.re := by
    have h1 : |(s - (2 + t * Complex.I)).re| ≤ 5 / 2 :=
      (abs_re_le_norm _).trans hdist
    rw [hresub] at h1
    have h2 := abs_le.mp h1
    linarith [h2.1]
  have him : |s.im - t| ≤ 5 / 2 := by
    have h1 : |(s - (2 + t * Complex.I)).im| ≤ 5 / 2 :=
      (abs_im_le_norm _).trans hdist
    rwa [himsub] at h1
  have him_abs : 15 / 2 ≤ |s.im| := by
    have h1 : |s.im| ≥ |t| - |s.im - t| := by
      have h2 : |t| ≤ |s.im| + |s.im - t| := by
        calc |t| = |s.im + (t - s.im)| := by ring_nf
          _ ≤ |s.im| + |t - s.im| := abs_add_le _ _
          _ = |s.im| + |s.im - t| := by rw [abs_sub_comm]
      linarith [h2]
    linarith [h1, him, ht]
  have hs1 : s ≠ 1 := by
    intro h
    rw [h] at him_abs
    norm_num at him_abs
  -- the identity applies (one of the two im-regions)
  have hrep : riemannZeta s = 1 / 2 + 1 / (s - 1)
      - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2) := by
    rcases lt_or_ge t 0 with ht0 | ht0
    · have h5 : s.im < -5 := by
        have h1 : s.im ≤ t + 5 / 2 := by
          rw [abs_le] at him
          linarith [him.2]
        have ht2 : t ≤ -10 := by
          rw [abs_of_neg ht0] at ht
          linarith
        linarith
      exact riemannZeta_eq_level2_of_im_lt (by linarith) h5
    · have h5 : 5 < s.im := by
        have h1 : s.im ≥ t - 5 / 2 := by
          rw [abs_le] at him
          linarith [him.1]
        have ht2 : 10 ≤ t := by rwa [abs_of_nonneg ht0] at ht
        linarith
      exact riemannZeta_eq_level2_of_im_gt (by linarith) h5
  rw [hrep]
  have hJ := norm_b2Integral_le (by linarith : -1 < s.re)
  have hsnorm : ‖s‖ ≤ |t| + 9 / 2 := by
    calc ‖s‖ = ‖(s - (2 + t * Complex.I)) + (2 + t * Complex.I)‖ := by rw [sub_add_cancel]
      _ ≤ ‖s - (2 + t * Complex.I)‖ + ‖2 + t * Complex.I‖ := norm_add_le _ _
      _ ≤ 5 / 2 + (2 + |t|) := by
          apply add_le_add hdist
          exact (Complex.norm_le_abs_re_add_abs_im _).trans (by
            simp [mul_re, mul_im, ofReal_re, ofReal_im, I_re, I_im])
      _ = |t| + 9 / 2 := by ring
  have hs1norm : ‖s + 1‖ ≤ |t| + 11 / 2 := by
    calc ‖s + 1‖ ≤ ‖s‖ + ‖(1 : ℂ)‖ := norm_add_le _ _
      _ ≤ |t| + 9 / 2 + 1 := by rw [norm_one]; linarith [hsnorm]
      _ = |t| + 11 / 2 := by ring
  have hsm1norm : 15 / 2 ≤ ‖s - 1‖ := by
    calc (15 : ℝ) / 2 ≤ |s.im| := him_abs
      _ = |(s - 1).im| := by simp [sub_im, one_im]
      _ ≤ ‖s - 1‖ := abs_im_le_norm _
  have hJ' : ‖∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖ ≤ 1 / 4 := by
    refine hJ.trans ?_
    rw [div_le_iff₀ (by linarith : (0:ℝ) < s.re + 1)]
    rw [div_mul_eq_mul_div, le_div_iff₀ (by norm_num : (0:ℝ) < 4)]
    linarith [hre]
  have hhalf : ‖(1 / 2 : ℂ)‖ = 1 / 2 := by
    rw [show (1 / 2 : ℂ) = ((1 / 2 : ℝ) : ℂ) by norm_num, Complex.norm_real, Real.norm_eq_abs]
    norm_num
  calc ‖1 / 2 + 1 / (s - 1) - s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖
      ≤ ‖1 / 2 + 1 / (s - 1)‖ + ‖s * (s + 1) * ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖ :=
        norm_sub_le _ _
    _ ≤ (1 / 2 + 1 / ‖s - 1‖) + ‖s‖ * ‖s + 1‖ * ‖∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-s - 2)‖ := by
        apply add_le_add
        · calc ‖1 / 2 + 1 / (s - 1)‖ ≤ ‖(1 / 2 : ℂ)‖ + ‖1 / (s - 1)‖ := norm_add_le _ _
            _ = 1 / 2 + ‖1 / (s - 1)‖ := by rw [hhalf]
            _ ≤ 1 / 2 + 1 / ‖s - 1‖ := by
                have hrec : ‖1 / (s - 1)‖ ≤ 1 / ‖s - 1‖ := by
                  rw [norm_div, norm_one]
                exact add_le_add_right hrec _
        · rw [norm_mul, norm_mul]
    _ ≤ (1 / 2 + 2 / 15) + (|t| + 9 / 2) * (|t| + 11 / 2) * (1 / 4) := by
        apply add_le_add
        · exact add_le_add_right
            ((one_div_le_one_div_of_le (by norm_num) hsm1norm).trans_eq
              (show (1 : ℝ) / (15 / 2) = 2 / 15 by norm_num)) _
        · exact mul_le_mul (mul_le_mul hsnorm hs1norm (norm_nonneg _) (by positivity))
            hJ' (norm_nonneg _) (mul_nonneg (by positivity) (by positivity))
    _ ≤ 3 / 4 * |t| ^ 2 := by
        nlinarith [ht, sq_nonneg (|t| - 10)]

end NguyenRH1

end