{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
  "old_string": "    _ \u2264 1 / ((m : \u211d) + 1) ^ 2 := by\n        apply div_le_div_of_nonneg_left (by norm_num : (0 : \u211d) \u2264 1)\n          (by positivity : (0 : \u211d) < ((m : \u211d) + 1) ^ 2)\n        rw [pow_two]\n        have h1 : (0 : \u211d) \u2264 (m : \u211d) + 1 := by positivity\n        exact mul_le_mul_of_nonneg_right hs1 h1.trans' (by linarith) |> le_rfl.trans' |> fun h => by\n          -- (m+1) \u2264 (m+1)\u00b7(m+1) since 1 \u2264 m+1\n          nlinarith [h1]",
  "new_string": "    _ \u2264 1 / ((m : \u211d) + 1) ^ 2 :=\n        (div_le_div_iff_of_pos_right (by positivity : (0 : \u211d) < ((m : \u211d) + 1) ^ 2)).mpr hs1"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean",
  "oldString": "    funext j\n    have hj : (2 : \u211d) ^ j \u2260 0 := pow_ne_zero _ two_ne_zero\n    field_simp\n    ring\n  rw [hsplit, Summable.tsum_add (hlinH.summable.mul_left _) (hgeom2H.summable.mul_left _)]\n  rw [tsum_mul_left, tsum_mul_left, hlin, hgeom2]\n  ring",
  "newString": "    funext j\n    have hj : (2 : \u211d) ^ j \u2260 0 := pow_ne_zero _ two_ne_zero\n    field_simp\n    ring_nf\n  rw [hsplit, Summable.tsum_add (hlinH.summable.mul_left _) (hgeom2H.mul_left _)]\n  rw [tsum_mul_left, tsum_mul_left, hlin, hgeom2]\n  ring",
  "originalFile": "/-\nNguyenRH1/LiCircleBound.lean \u2014 tier ii\u2032 sub-stage ii\u2032-5e-v (D-068 \u00a75):\nthe circle bound for the partial-fraction difference and the squeeze to\nthe capstone identity.\n\n\u00a70: conjugate symmetry of the nontrivial zeros (for the lower-half\n    circle arcs).\n\u00a71: the mult-weighted ordinate-window count bridges from Zeta23's RvM\n    local count (`zeta_local_zero_count`: Ncount(t, t+1] \u2264 A\u2080\u00b7log(|t|+3)\n    with multiplicity, ALL t \u2014 no perimeter): `A0count` + the dyadic\n    interval count `Ncount_le_of_interval`.\n\u00a72: the Dirichlet bound `norm_logDeriv_zeta_le_dirichlet` (\u2016\u03b6\u2032/\u03b6 s\u2016 \u2264\n    dirichletC2 for re s \u2265 2; \u2212\u03b6\u2032/\u03b6 = LSeries \u039b, termwise \u2264 the s = 2\n    majorant) \u2014 the right near-axis arc input.\n\u00a73+: (this file, subsequent sub-stages) the series bound, the logDeriv\n    assembly, the Fexpr circle bound, the Schwarz squeeze, and the\n    capstone `partialFraction_identity`.\n\nArchive references: D-068 \u00a75, journal-029.\n-/\nimport Mathlib\nimport Zeta23.RvM.LocalCount\nimport NguyenRH1.LiFEntire\nimport NguyenRH1.LiGapCircles\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 0. Conjugate symmetry -/\n\n/-- The conjugate of a nontrivial zero is a nontrivial zero. -/\nlemma isNontrivialZero_conj {\u03c1 : \u2102} (h\u03c1 : IsNontrivialZero \u03c1) :\n    IsNontrivialZero ((starRingEnd \u2102) \u03c1) := by\n  refine \u27e8?_, ?_, ?_\u27e9\n  \u00b7 rw [_root_.riemannZeta_conj, h\u03c1.1, map_zero]\n  \u00b7 rw [Complex.conj_re]; exact h\u03c1.2.1\n  \u00b7 rw [Complex.conj_re]; exact h\u03c1.2.2\n\n/-! ## 1. The mult-weighted window count bridges -/\n\n/-- The local-count constant: from Zeta23's RvM local count\n(`zeta_local_zero_count`, [Tit86 Thm 9.2] \u2014 mult-weighted, two-sided,\nall t, PROVED unconditionally in Zeta23). -/\ndef A0count : \u211d := Classical.choose Zeta23.RvM.zeta_local_zero_count\n\nlemma A0count_ge_one : (1 : \u211d) \u2264 A0count :=\n  (Classical.choose_spec Zeta23.RvM.zeta_local_zero_count).1\n\nlemma A0count_pos : (0 : \u211d) < A0count := lt_of_lt_of_le one_pos A0count_ge_one\n\n/-- The unit-window bound: Ncount(t, t+1] \u2264 A\u2080\u00b7log(|t|+3). -/\nlemma Ncount_window_le (t : \u211d) :\n    (Zeta23.Ncount t (t + 1) : \u211d) \u2264 A0count * Real.log (|t| + 3) :=\n  (Classical.choose_spec Zeta23.RvM.zeta_local_zero_count).2 t\n\n/-- Window additivity: Ncount(a, c] = Ncount(a, b] + Ncount(b, c] for\na \u2264 b \u2264 c (the disjoint union of the ordinate windows). -/\nlemma Ncount_add_of_le {a b c : \u211d} (hab : a \u2264 b) (hbc : b \u2264 c) :\n    Zeta23.Ncount a c = Zeta23.Ncount a b + Zeta23.Ncount b c := by\n  have hunion : Zeta23.zerosIn a c = Zeta23.zerosIn a b \u222a Zeta23.zerosIn b c := by\n    ext \u03c1\n    constructor\n    \u00b7 intro h\u03c1c\n      obtain \u27e8h\u03c1, ha, hc\u27e9 := h\u03c1c\n      rcases le_or_gt \u03c1.im b with h | h\n      \u00b7 exact Set.mem_union_left _ \u27e8h\u03c1, ha, h\u27e9\n      \u00b7 exact Set.mem_union_right _ \u27e8h\u03c1, h, hc\u27e9\n    \u00b7 intro h\n      rcases h with h\u03c1b | h\u03c1c\n      \u00b7 obtain \u27e8h\u03c1, ha, hb\u27e9 := h\u03c1b\n        exact \u27e8h\u03c1, ha, hb.trans hbc\u27e9\n      \u00b7 obtain \u27e8h\u03c1, hb, hc\u27e9 := h\u03c1c\n        exact \u27e8h\u03c1, hab.trans_lt hb, hc\u27e9\n  have hdisj : Disjoint (Zeta23.zerosIn a b) (Zeta23.zerosIn b c) := by\n    rw [Set.disjoint_iff]\n    intro \u03c1 \u27e8h1, h2\u27e9\n    exact absurd (h1.2.2.trans_lt h2.2.1) (lt_irrefl \u03c1.im)\n  rw [Zeta23.Ncount, Zeta23.Ncount, Zeta23.Ncount, hunion]\n  exact_mod_cast finsum_mem_union hdisj (Zeta23.zerosIn_finite a b)\n    (Zeta23.zerosIn_finite b c)\n\n/-- The N-step unit-window chain: Ncount(a, a+N] \u2264 A\u2080\u00b7N\u00b7log(|a|+N+3). -/\nlemma Ncount_chain_le (a : \u211d) (N : \u2115) :\n    (Zeta23.Ncount a (a + (N : \u211d)) : \u211d)\n      \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := by\n  induction N with\n  | zero =>\n    simp only [Nat.cast_zero, add_zero]\n    have h0 : Zeta23.zerosIn a a = \u2205 := by\n      ext \u03c1\n      constructor\n      \u00b7 intro h\n        obtain \u27e8-, h1, h2\u27e9 := h\n        exact absurd (h2.trans_lt h1) (lt_irrefl _)\n      \u00b7 intro h\n        simp at h\n    have hz : Zeta23.Ncount a a = 0 := by\n      simp only [Zeta23.Ncount, h0, finsum_mem_empty]\n    rw [hz, Nat.cast_zero]\n    simp\n  | succ N ih =>\n    have hN0 : (0 : \u211d) \u2264 (N : \u211d) := Nat.cast_nonneg N\n    have hsplit : Zeta23.Ncount a (a + (N : \u211d) + 1)\n        = Zeta23.Ncount a (a + (N : \u211d)) + Zeta23.Ncount (a + (N : \u211d)) (a + (N : \u211d) + 1) :=\n      Ncount_add_of_le (a := a) (b := a + (N : \u211d)) (c := a + (N : \u211d) + 1)\n        (by linarith) (by linarith)\n    have hcast : a + ((N + 1 : \u2115) : \u211d) = a + (N : \u211d) + 1 := by push_cast; ring\n    rw [hcast, hsplit]\n    have hwin := Ncount_window_le (a + (N : \u211d))\n    have hlog : Real.log (|a + (N : \u211d)| + 3) \u2264 Real.log (|a| + (N : \u211d) + 3) := by\n      apply Real.log_le_log (by positivity)\n      have h1 : |a + (N : \u211d)| \u2264 |a| + (N : \u211d) :=\n        (abs_add_le _ _).trans (by rw [abs_of_nonneg (show (0 : \u211d) \u2264 (N : \u211d) from Nat.cast_nonneg N)])\n      linarith\n    have hlogpos : (0 : \u211d) \u2264 Real.log (|a| + (N : \u211d) + 3) := by\n      apply Real.log_nonneg\n      have h1 : (1 : \u211d) \u2264 |a| + 3 := by linarith [abs_nonneg a]\n      linarith [hN0]\n    have hlogpos' : (0 : \u211d) \u2264 Real.log (|a| + ((N : \u211d) + 1) + 3) := by\n      apply Real.log_nonneg\n      have h1 : (1 : \u211d) \u2264 |a| + 3 := by linarith [abs_nonneg a]\n      linarith [hN0]\n    push_cast\n    -- goal: \u2191(Ncount a (a+\u2191N)) + \u2191(Ncount (a+\u2191N) (a+\u2191N+1)) \u2264 A\u2080(\u2191N+1)\u00b7log(|a|+(\u2191N+1)+3)\n    have hlogC : Real.log (|a| + (N : \u211d) + 3)\n        \u2264 Real.log (|a| + ((N : \u211d) + 1) + 3) :=\n      Real.log_le_log (by positivity) (by linarith)\n    have hle1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n        \u2264 A0count * (N : \u211d) * Real.log (|a| + ((N : \u211d) + 1) + 3) :=\n      mul_le_mul_of_nonneg_left hlogC (mul_nonneg A0count_pos.le hN0)\n    have hle2 : A0count * Real.log (|a + (N : \u211d)| + 3)\n        \u2264 A0count * Real.log (|a| + ((N : \u211d) + 1) + 3) := by\n      apply mul_le_mul_of_nonneg_left _ A0count_pos.le\n      apply Real.log_le_log (by positivity)\n      have h1 : |a + (N : \u211d)| \u2264 |a| + (N : \u211d) :=\n        (abs_add_le _ _).trans (by rw [abs_of_nonneg (show (0 : \u211d) \u2264 (N : \u211d) from Nat.cast_nonneg N)])\n      linarith\n    have hsum : \u2191(Zeta23.Ncount a (a + (N : \u211d))) + \u2191(Zeta23.Ncount (a + (N : \u211d)) (a + (N : \u211d) + 1))\n        \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n          + A0count * Real.log (|a + (N : \u211d)| + 3) :=\n      add_le_add ih hwin\n    linarith [hsum, hle1, hle2]\n\n/-- The dyadic-interval count: Ncount(a, b] \u2264 A\u2080\u00b7(b\u2212a+1)\u00b7log(b+4) for\n0 \u2264 a \u2264 b (the unit-window chain + the ceil cover). -/\nlemma Ncount_le_of_interval {a b : \u211d} (ha : 0 \u2264 a) (hab : a \u2264 b) :\n    (Zeta23.Ncount a b : \u211d) \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n  set N : \u2115 := \u2308b - a\u2309\u208a with hN\n  have hNb : b \u2264 a + (N : \u211d) := by\n    have h := Nat.le_ceil (b - a)\n    rw [\u2190 hN] at h\n    have h2 : (b - a : \u211d) \u2264 (N : \u211d) := h\n    linarith\n  have hsub : Zeta23.zerosIn a b \u2286 Zeta23.zerosIn a (a + (N : \u211d)) := by\n    intro \u03c1 h\u03c1\n    refine \u27e8h\u03c1.1, h\u03c1.2.1, ?_\u27e9\n    exact h\u03c1.2.2.trans hNb\n  have hle : Zeta23.Ncount a b \u2264 Zeta23.Ncount a (a + (N : \u211d)) := by\n    rw [Zeta23.Ncount, Zeta23.Ncount]\n    rw [finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a b),\n      finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a (a + (N : \u211d)))]\n    apply Finset.sum_le_sum_of_subset_of_nonneg\n    \u00b7 intro \u03c1 h\u03c1\n      rw [Set.Finite.mem_toFinset] at h\u03c1 \u22a2\n      exact hsub h\u03c1\n    \u00b7 intro \u03c1 _ _\n      exact Nat.cast_nonneg _\n  have hchain := Ncount_chain_le a N\n  have hNle : (N : \u211d) \u2264 b - a + 1 := by\n    have h := Nat.ceil_lt_add_one (sub_nonneg.mpr hab)\n    rw [\u2190 hN] at h\n    have h2 : ((N : \u211d)) < b - a + 1 := by exact_mod_cast h\n    linarith\n  have hlogle : Real.log (|a| + (N : \u211d) + 3) \u2264 Real.log (b + 4) := by\n    apply Real.log_le_log (by positivity)\n    rw [abs_of_nonneg ha]\n    linarith\n  calc (Zeta23.Ncount a b : \u211d)\n      \u2264 (Zeta23.Ncount a (a + (N : \u211d)) : \u211d) := by exact_mod_cast hle\n    _ \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := hchain\n    _ \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n        have hlogpos : (0 : \u211d) \u2264 Real.log (b + 4) := by\n          apply Real.log_nonneg; linarith\n        have h1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n            \u2264 A0count * (N : \u211d) * Real.log (b + 4) :=\n          mul_le_mul_of_nonneg_left hlogle (mul_nonneg A0count_pos.le (Nat.cast_nonneg N))\n        have h2 : A0count * (N : \u211d) * Real.log (b + 4)\n            \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n          apply mul_le_mul_of_nonneg_right _ hlogpos\n          nlinarith [A0count_pos, hNle, sub_nonneg.mpr hab]\n        exact h1.trans h2\n\n/-! ## 2. The Dirichlet bound -/\n\n/-- The Dirichlet majorant constant: the absolute sum of the von\nMangoldt L-series terms at s = 2 (summable since 2 > 1). -/\ndef dirichletC2 : \u211d :=\n  \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 C\u2082 for re s \u2265 2 (the Dirichlet-series majorant:\n\u2212\u03b6\u2032/\u03b6 = LSeries \u039b for re > 1, termwise \u2264 the s = 2 sum). -/\nlemma norm_logDeriv_zeta_le_dirichlet {s : \u2102} (hs : 2 \u2264 s.re) :\n    \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC2 := by\n  have hs1 : (1 : \u211d) < s.re := by linarith\n  have h1 : -logDeriv riemannZeta s\n      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s := by\n    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n    rw [logDeriv, Pi.div_apply, h2]\n    ring\n  have hsum2 : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsumS : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n  have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016\n      \u2264 dirichletC2 := by\n    show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 \u2264 _\n    calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016\n        \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 :=\n          norm_tsum_le_tsum_norm hsumS\n      _ \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n          Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n            simp\n            exact hs) n) hsumS hsum2\n      _ = dirichletC2 := rfl\n  calc \u2016logDeriv riemannZeta s\u2016\n      = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016 := by\n        rw [\u2190 h1, norm_neg]\n    _ \u2264 dirichletC2 := hle\n\n/-! ## 3. The tsum split + the generalized interval count + the low-zero\nconstant -/\n\n/-- Splitting a summable real tsum over a finset:\n\u2211' f = \u2211_{i \u2208 s} f i + \u2211' (if i \u2208 s then 0 else f i). -/\nlemma tsum_split_finset {\u03b9 : Type*} [DecidableEq \u03b9] {f : \u03b9 \u2192 \u211d} (hf : Summable f)\n    (s : Finset \u03b9) :\n    \u2211' i, f i = \u2211 i \u2208 s, f i + \u2211' i, (if i \u2208 s then 0 else f i) := by\n  classical\n  have h1 : Summable (fun i => if i \u2208 s then f i else 0) := by\n    apply Summable.of_norm_bounded hf.norm\n    intro i\n    by_cases hi : i \u2208 s <;> simp [hi]\n  have h2 : Summable (fun i => if i \u2208 s then 0 else f i) := by\n    apply Summable.of_norm_bounded hf.norm\n    intro i\n    by_cases hi : i \u2208 s <;> simp [hi]\n  have h3 : \u2211' i, f i\n      = \u2211' i, ((if i \u2208 s then f i else 0) + (if i \u2208 s then 0 else f i)) := by\n    apply tsum_congr\n    intro i\n    by_cases hi : i \u2208 s <;> simp [hi]\n  rw [h3, Summable.tsum_add h1 h2]\n  congr 1\n  rw [tsum_eq_sum (s := s) (fun b hb => if_neg hb)]\n  exact Finset.sum_congr rfl (fun b hb => if_pos hb)\n\n/-- The generalized dyadic-interval count (both signs):\nNcount(a, b] \u2264 A\u2080\u00b7(b\u2212a+1)\u00b7log(3\u00b7max|a||b| + 5). -/\nlemma Ncount_le_of_interval_gen {a b : \u211d} (hab : a \u2264 b) :\n    (Zeta23.Ncount a b : \u211d)\n      \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n  set N : \u2115 := \u2308b - a\u2309\u208a with hN\n  have hNb : b \u2264 a + (N : \u211d) := by\n    have h := Nat.le_ceil (b - a)\n    rw [\u2190 hN] at h\n    linarith\n  have hsub : Zeta23.zerosIn a b \u2286 Zeta23.zerosIn a (a + (N : \u211d)) := by\n    intro \u03c1 h\u03c1\n    exact \u27e8h\u03c1.1, h\u03c1.2.1, h\u03c1.2.2.trans hNb\u27e9\n  have hle : Zeta23.Ncount a b \u2264 Zeta23.Ncount a (a + (N : \u211d)) := by\n    rw [Zeta23.Ncount, Zeta23.Ncount]\n    rw [finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a b),\n      finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a (a + (N : \u211d)))]\n    apply Finset.sum_le_sum_of_subset_of_nonneg\n    \u00b7 intro \u03c1 h\u03c1\n      rw [Set.Finite.mem_toFinset] at h\u03c1 \u22a2\n      exact hsub h\u03c1\n    \u00b7 intro \u03c1 _ _\n      exact Nat.cast_nonneg _\n  have hchain := Ncount_chain_le a N\n  have hNle : (N : \u211d) \u2264 b - a + 1 := by\n    have h := Nat.ceil_lt_add_one (sub_nonneg.mpr hab)\n    rw [\u2190 hN] at h\n    have h2 : ((N : \u211d)) < b - a + 1 := by exact_mod_cast h\n    linarith\n  have hlogle : Real.log (|a| + (N : \u211d) + 3)\n      \u2264 Real.log (3 * max |a| |b| + 5) := by\n    apply Real.log_le_log (by positivity)\n    have hM1 : |a| \u2264 max |a| |b| := le_max_left _ _\n    have hM2 : |b| \u2264 max |a| |b| := le_max_right _ _\n    have hba : b - a \u2264 |b| + |a| := by\n      have h1 := le_abs_self b\n      have h2 : -a \u2264 |a| := by rw [\u2190 abs_neg a]; exact le_abs_self (-a)\n      linarith\n    nlinarith [hNle, hM1, hM2, hba, abs_nonneg a, abs_nonneg b]\n  have hlogpos : (0 : \u211d) \u2264 Real.log (3 * max |a| |b| + 5) := by\n    apply Real.log_nonneg\n    have h1 : (0 : \u211d) \u2264 max |a| |b| := le_trans (abs_nonneg a) (le_max_left _ _)\n    linarith\n  calc (Zeta23.Ncount a b : \u211d)\n      \u2264 (Zeta23.Ncount a (a + (N : \u211d)) : \u211d) := by exact_mod_cast hle\n    _ \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := hchain\n    _ \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n        have h1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n            \u2264 A0count * (N : \u211d) * Real.log (3 * max |a| |b| + 5) :=\n          mul_le_mul_of_nonneg_left hlogle (mul_nonneg A0count_pos.le (Nat.cast_nonneg N))\n        have h2 : A0count * (N : \u211d) * Real.log (3 * max |a| |b| + 5)\n            \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n          apply mul_le_mul_of_nonneg_right _ hlogpos\n          nlinarith [A0count_pos, hNle, sub_nonneg.mpr hab]\n        exact h1.trans h2\n\n/-- The low-zero finset: nontrivial zeros with \u2016\u03c1\u2016 \u2264 3. -/\ndef lowZeros : Finset {\u03c1 : \u2102 // IsNontrivialZero \u03c1} :=\n  (show {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | \u2016(\u03c1 : \u2102)\u2016 \u2264 3}.Finite from\n    (finite_subtype_norm_lt 4).subset\n      (fun \u03c1 h\u03c1 => lt_of_le_of_lt (show \u2016(\u03c1 : \u2102)\u2016 \u2264 3 from h\u03c1) (by norm_num))).toFinset\n\n/-- The low-zero symbolic constant (a fixed finite sum of fixed positive\nreals; \u2016\u03c1\u2016 > 0 for nontrivial \u03c1 since re \u03c1 > 0). -/\ndef lowZeroConst : \u211d :=\n  \u2211 \u03c1 \u2208 lowZeros, (zeroMult (\u03c1 : \u2102) : \u211d) * (1 + 1 / \u2016(\u03c1 : \u2102)\u2016)\n\nlemma lowZeroConst_nonneg : 0 \u2264 lowZeroConst :=\n  Finset.sum_nonneg fun _\u03c1 _ => mul_nonneg (Nat.cast_nonneg _)\n    (add_nonneg one_pos.le (div_nonneg one_pos.le (norm_nonneg _)))\n\n/-! ## 4. The far-tail bound -/\n\n/-- The dyadic log series closed form:\n\u2211' j, ((j+4)\u00b7log 2 + log X)/2^j = 10\u00b7log 2 + 2\u00b7log X. -/\nlemma tsum_dyadic_log (X : \u211d) :\n    \u2211' j : \u2115, ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j\n      = 10 * Real.log 2 + 2 * Real.log X := by\n  have hgeom2H : Summable (fun j : \u2115 => ((1 : \u211d) / 2) ^ j) := summable_geometric_two\n  have hgeom2 : \u2211' j : \u2115, ((1 : \u211d) / 2) ^ j = 2 := tsum_geometric_two\n  have hlinH := hasSum_coe_mul_geometric_of_norm_lt_one (r := (1 : \u211d) / 2) (by norm_num)\n  have hlin : \u2211' j : \u2115, (j : \u211d) * ((1 : \u211d) / 2) ^ j = 2 := by\n    have h := hlinH.tsum_eq\n    norm_num at h\n    exact h\n  have hsplit : (fun j : \u2115 => ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j)\n      = fun j : \u2115 => Real.log 2 * ((j : \u211d) * ((1 : \u211d) / 2) ^ j)\n        + (4 * Real.log 2 + Real.log X) * ((1 : \u211d) / 2) ^ j := by\n    funext j\n    have hj : (2 : \u211d) ^ j \u2260 0 := pow_ne_zero _ two_ne_zero\n    field_simp\n    ring\n  rw [hsplit, Summable.tsum_add (hlinH.summable.mul_left _) (hgeom2H.summable.mul_left _)]\n  rw [tsum_mul_left, tsum_mul_left, hlin, hgeom2]\n  ring\n\n/-- log 2 \u2264 1 (since 2 \u2264 e). -/\nlemma log_two_le_one : Real.log 2 \u2264 1 := by\n  rw [show (1 : \u211d) = Real.log (Real.exp 1) by rw [Real.log_exp]]\n  apply Real.log_le_log (by norm_num)\n  have h := Real.exp_one_gt_d9\n  linarith\n\n/-- For X \u2265 200: (4A\u2080/X)\u00b7(10\u00b7log 2 + 2\u00b7log X) \u2264 16\u00b7A\u2080\u00b7log X / X. -/\nlemma dyadic_tail_constant {X : \u211d} (hX : 200 \u2264 X) :\n    (4 * A0count / X) * (10 * Real.log 2 + 2 * Real.log X)\n      \u2264 16 * A0count * Real.log X / X := by\n  have hX0 : (0 : \u211d) < X := by linarith\n  have hlogX : 5 \u2264 Real.log X := by\n    rw [show (5 : \u211d) = Real.log (Real.exp 5) by rw [Real.log_exp]]\n    apply Real.log_le_log (Real.exp_pos _)\n    have h1 : Real.exp 5 = (Real.exp 1) ^ 5 := by\n      rw [\u2190 Real.exp_nat_mul]\n      norm_num\n    have h2 := Real.exp_one_lt_d9.le\n    have h3 : (Real.exp 1) ^ 5 \u2264 (2.7182818286 : \u211d) ^ 5 :=\n      pow_le_pow_left\u2080 (Real.exp_pos 1).le h2 5\n    have h4 : (2.7182818286 : \u211d) ^ 5 \u2264 200 := by norm_num\n    linarith [h1, h3, h4]\n  have hlog2 := log_two_le_one\n  have hA0 : (0 : \u211d) \u2264 4 * A0count / X :=\n    div_nonneg (mul_nonneg (by norm_num) A0count_pos.le) hX0.le\n  have h1 : 10 * Real.log 2 + 2 * Real.log X \u2264 4 * Real.log X := by linarith\n  calc (4 * A0count / X) * (10 * Real.log 2 + 2 * Real.log X)\n      \u2264 (4 * A0count / X) * (4 * Real.log X) := mul_le_mul_of_nonneg_left h1 hA0\n    _ = 16 * A0count * Real.log X / X := by ring\n\n/-- The dyadic class of a zero relative to scale X:\nNat.log 2 \u230a|im \u03c1|/X\u230b\u208a, so 2^j\u00b7X \u2264 |im \u03c1| < 2^{j+1}\u00b7X when |im \u03c1| \u2265 X. -/\ndef dyadClass (X : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2115 :=\n  Nat.log 2 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a\n\nlemma dyadClass_lower {X : \u211d} (hX : 0 < X) {\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}}\n    (h\u03c1 : X \u2264 |(\u03c1 : \u2102).im|) :\n    (2 : \u211d) ^ dyadClass X \u03c1 * X \u2264 |(\u03c1 : \u2102).im| := by\n  have hfl : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a \u2260 0 := by\n    rw [Ne, Nat.floor_eq_zero]\n    push Not\n    have h1 : (1 : \u211d) \u2264 |(\u03c1 : \u2102).im| / X := (le_div_iff\u2080 hX).mpr (by linarith)\n    linarith\n  have h2 := Nat.pow_log_le_self 2 hfl\n  have h3 : ((2 ^ dyadClass X \u03c1 : \u2115) : \u211d) \u2264 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a := by exact_mod_cast h2\n  have h4 : (\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a : \u211d) \u2264 |(\u03c1 : \u2102).im| / X := Nat.floor_le (by positivity)\n  have h5 : ((2 ^ dyadClass X \u03c1 : \u2115) : \u211d) = (2 : \u211d) ^ dyadClass X \u03c1 := by push_cast; ring\n  rw [h5] at h3\n  rw [le_div_iff\u2080 hX] at h4\n  have h6 : (2 : \u211d) ^ dyadClass X \u03c1 * X \u2264 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a * X :=\n    mul_le_mul_of_nonneg_right h3 hX.le\n  linarith\n\nlemma dyadClass_upper {X : \u211d} (hX : 0 < X) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n    |(\u03c1 : \u2102).im| < (2 : \u211d) ^ (dyadClass X \u03c1 + 1) * X := by\n  have h2 : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a < 2 ^ (dyadClass X \u03c1 + 1) :=\n    Nat.lt_pow_succ_log_self (by norm_num) _\n  have h3 : ((\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a : \u211d) + 1) \u2264 (2 : \u211d) ^ (dyadClass X \u03c1 + 1) := by\n    have h4 : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a + 1 \u2264 2 ^ (dyadClass X \u03c1 + 1) := h2\n    have h5 : ((\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a + 1 : \u2115) : \u211d) \u2264 ((2 ^ (dyadClass X \u03c1 + 1) : \u2115) : \u211d) := by\n      exact_mod_cast h4\n    push_cast at h5\n    linarith\n  have h6 : |(\u03c1 : \u2102).im| / X < \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a + 1 := Nat.lt_floor_add_one _\n  have h7 : ((2 ^ (dyadClass X \u03c1 + 1) : \u2115) : \u211d) = (2 : \u211d) ^ (dyadClass X \u03c1 + 1) := by\n    push_cast; ring\n  rw [h7] at h3\n  have h8 := (div_lt_iff\u2080 hX).mpr ((Nat.lt_floor_add_one _).trans_le h3)\n  linarith\n\n/-- The tail summand (if-form on the zero subtype). -/\ndef tailTerm (X : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u211d :=\n  if X < |(\u03c1 : \u2102).im| then (zeroMult \u03c1 : \u211d) / (1 + \u03c1.im ^ 2) else 0\n\nlemma tailTerm_nonneg {X : \u211d} (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n    0 \u2264 tailTerm X \u03c1 := by\n  by_cases h : X < |(\u03c1 : \u2102).im| <;>\n    simp [tailTerm, h, div_nonneg (Nat.cast_nonneg _)\n      (by positivity : (0 : \u211d) \u2264 1 + \u03c1.im ^ 2)]\n\n/-- The tail summand is summable (dominated by 2\u00b7m/(1+\u2016\u03b3\u2016\u00b2) via\n1 + \u2016\u03b3\u2016\u00b2 \u2264 2(1 + im\u00b2)). -/\nlemma tailTerm_summable (X : \u211d) :\n    Summable (tailTerm X) := by\n  have hbase : Summable (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n      2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))) :=\n    (WeilEF.zero_sum_inv_sq zetaSeam).mul_left 2\n  apply Summable.of_norm_bounded hbase\n  intro \u03c1\n  rw [tailTerm]\n  by_cases h : X < |(\u03c1 : \u2102).im|\n  \u00b7 rw [if_pos h]\n    have hgam : Complex.normSq (gammaOf (\u03c1 : \u2102))\n        = (\u03c1 : \u2102).im ^ 2 + (1 / 2 - (\u03c1 : \u2102).re) ^ 2 := by\n      rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]\n      ring\n    have hcmp : 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) \u2264 2 * (1 + (\u03c1 : \u2102).im ^ 2) := by\n      rw [hgam]\n      have hre : ((\u03c1 : \u2102).re - 1 / 2) ^ 2 \u2264 1 / 4 := by\n        have h0 := \u03c1.2.2.1\n        have h1 := \u03c1.2.2.2\n        nlinarith [sq_nonneg ((\u03c1 : \u2102).re - 1 / 2)]\n      nlinarith [sq_nonneg (\u03c1 : \u2102).im]\n    have hpos1 : (0 : \u211d) < 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) := by\n      have h := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102)); linarith\n    have hpos2 : (0 : \u211d) < 1 + (\u03c1 : \u2102).im ^ 2 := by positivity\n    have hfrac : 1 / (1 + (\u03c1 : \u2102).im ^ 2) \u2264 2 / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))) := by\n      rw [div_le_div_iff\u2080 hpos2 hpos1]\n      nlinarith [hcmp]\n    have hm : (0 : \u211d) \u2264 (zeroMult \u03c1 : \u211d) := Nat.cast_nonneg _\n    calc \u2016(zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)\u2016\n        = (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2) :=\n          norm_of_nonneg (div_nonneg (Nat.cast_nonneg _) hpos2.le)\n      _ \u2264 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) := by\n          rw [show (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)\n              = (zeroMult \u03c1 : \u211d) * (1 / (1 + (\u03c1 : \u2102).im ^ 2)) from by ring]\n          rw [show 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))\n              = (zeroMult \u03c1 : \u211d) * (2 / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) from by ring]\n          exact mul_le_mul_of_nonneg_left hfrac hm\n  \u00b7 rw [if_neg h]\n    positivity\n\nend NguyenRH1\n\nend\n",
  "structuredPatch": [
    {
      "oldStart": 352,
      "oldLines": 8,
      "newStart": 352,
      "newLines": 8,
      "lines": [
        "     funext j",
        "     have hj : (2 : \u211d) ^ j \u2260 0 := pow_ne_zero _ two_ne_zero",
        "     field_simp",
        "-    ring",
        "-  rw [hsplit, Summable.tsum_add (hlinH.summable.mul_left _) (hgeom2H.summable.mul_left _)]",
        "+    ring_nf",
        "+  rw [hsplit, Summable.tsum_add (hlinH.summable.mul_left _) (hgeom2H.mul_left _)]",
        "   rw [tsum_mul_left, tsum_mul_left, hlin, hgeom2]",
        "   ring",
        " "
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}

{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
  "old_string": "  have hderiv : deriv Complex.Gamma (\u2191x : \u2102) = \u2191(deriv Real.Gamma x) := by\n    have h1 : HasDerivAt (fun y : \u211d => Complex.Gamma (\u2191y)) (\u2191(deriv Real.Gamma x)) x := by\n      have h2 : HasDerivAt Real.Gamma (deriv Real.Gamma x) x := by\n        apply Real.differentiableAt_Gamma (fun m => ?_) |>.hasDerivAt\n        intro hmeq\n        rw [hmeq] at hx0\n        simp at hx0\n        have hm : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n        linarith\n      have h3 := Complex.ofRealCLM.hasDerivAt.comp x h2\n      -- HasDerivAt (ofReal \u2218 Gamma) (\u2191(Gamma' x)) x\n      rw [Complex.ofRealCLM_apply] at h3\n      -- ofRealCLM 1 = 1\n      have h4 : (Complex.ofRealCLM (1 : \u211d)) = (1 : \u2102) := by\n        rw [Complex.ofRealCLM_apply]; simp\n      rw [h4, smul_eq_mul, mul_one] at h3\n      have heq : (Complex.ofRealCLM \u2218 Real.Gamma) = fun y : \u211d => \u2191(Real.Gamma y) := by\n        funext y\n        rw [Complex.ofRealCLM_apply]\n      rw [heq] at h3\n      -- link Gamma \u2218 ofReal to ofReal \u2218 Gamma\n      have h5 : (fun y : \u211d => Complex.Gamma (\u2191y)) = fun y : \u211d => \u2191(Real.Gamma y) :=\n        fun y => Complex.Gamma_ofReal y\n      rw [h5] at h3\n      exact h3",
  "new_string": "  have hderiv : deriv Complex.Gamma (\u2191x : \u2102) = \u2191(deriv Real.Gamma x) := by\n    have h2 : HasDerivAt Real.Gamma (deriv Real.Gamma x) x := by\n      have hd : DifferentiableAt \u211d Real.Gamma x := by\n        apply Real.differentiableAt_Gamma\n        intro m hmeq\n        rw [hmeq] at hx0\n        simp at hx0\n        have hm : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n        linarith\n      exact hd.hasDerivAt\n    have h1 : HasDerivAt (fun y : \u211d => \u2191(Real.Gamma y)) (\u2191(deriv Real.Gamma x)) x := by\n      have h3 := Complex.ofRealCLM.hasFDerivAt.comp_hasDerivAt x h2\n      rw [Complex.ofRealCLM_apply] at h3\n      have heq : (Complex.ofRealCLM \u2218 Real.Gamma) = fun y : \u211d => \u2191(Real.Gamma y) := by\n        funext y\n        rw [Function.comp_apply, Complex.ofRealCLM_apply]\n      rw [heq] at h3\n      exact h3"
}