[{"type":"thinking","thinking":"- `TendstoLocallyUniformlyOn.congr (hf) (hg : ∀ n, s.EqOn (F n) (G n)) : TendstoLocallyUniformlyOn G f p s` ✓\n- `TendstoLocallyUniformlyOn.congr_right (hf) (hg : s.EqOn f g)` ✓\n- No `tendstoLocallyUniformlyOn_const` found. For the constant sequence: TendstoLocallyUniformlyOn (fun _ => f) f p s — via tendstoLocallyUniformlyOn_iff_forall_tendsto? or simply: the constant sequence converges uniformly: `tendstoUniformlyOn_const`? hmm — there might be `tendstoUniformlyOn_const : TendstoUniformlyOn (fun _ => f) f l s`? — not found either. The general: `tendsto_const_nhds` gives Tendsto (fun _ => f x)... — for the uniform-on version: prove via tendstoLocallyUniformlyOn_iff_forall_tendsto or the Metric version. There's definitely something like `tendstoUniformlyOn_const` hmm — let me just use: TendstoLocallyUniformlyOn (fun _ => f) f p s := by rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] ... too deep. EASIER: TendstoLocallyUniformlyOn.of... — hmm. Let me search for how others prove const convergence... Actually: `tendstoLocallyUniformlyOn_const` might exist under a different name — `TendstoLocallyUniformlyOn.const`? For the const-in-n: (fun _ : ℕ => f) → f: this is just: every sequence constantly f converges to f uniformly — I'll prove inline:\n```lean\n  have hB : TendstoLocallyUniformlyOn (fun _ : ℕ => fun x : ℝ => -1 / x) (fun x => -1 / x)\n      atTop (Set.Ioi 0) := by\n    rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi]\n    intro K hK hKc\n    rw [Metric.tendstoUniformlyOn_iff]\n    intro ε hε\n    exact ⟨0, fun n _ x _ => by simpa using hε⟩  -- dist is 0 < ε\n```\nHmm the ∀ᶠ n in atTop, ∀ x ∈ K, dist (...) (...) < ε — the anonymous ⟨0, ...⟩ needs eventually_atTop form — `Filter.eventually_atTop.mpr ⟨0, fun n hn x hx => ...⟩`? — the ∀ᶠ n in atTop, P n — `eventually_atTop.mpr ⟨N, ...⟩` ✓. The goal after Metric.tendstoUniformlyOn_iff: ∀ ε > 0, ∀ᶠ n in atTop, ∀ x ∈ K, dist ((fun _ => fun x => -1/x) n x) ((fun x => -1/x) x) < ε — the functions beta to -1/x and -1/x — dist = 0 < ε ✓ `by simpa using hε` — simpa normalizes the dist term to 0: dist a a = 0 ✓ simp [dist_self] — simpa using hε : 0 < ε ✓.\n\nHmm wait — `Metric.tendstoUniformlyOn_iff : TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x ∈ s, dist (F n x) (f x) < ε` ✓.\n\nAnd for hA the same pattern ✓ (already structured that way).\n\nNow the hdecomp/show approach for the final assembly. Also the congr for the limit: the assembly (hA.add (hB.add hC)) : TendstoLocallyUniformlyOn (fun n x => A n x + (B n x + C n x)) (fun x => (−γ) + (−1/x + tsum)) atTop (Ioi 0) — wait — hA.add (hB.add hC): TendstoLocallyUniformlyOn.add (hf : ... F f) (hg : ... G g) : TendstoLocallyUniformlyOn (fun n x => F n x + G n x) (fun x => f x + g x) — `TendstoLocallyUniformlyOn.add` exists? — `TendstoLocallyUniformlyOn.add (hf : TendstoLocallyUniformlyOn F f p s) (hg : TendstoLocallyUniformlyOn G g p s) : TendstoLocallyUniformlyOn (F + G) (f + g) p s`? — the function forms: (F + G) n x — Pi.add — vs fun n x => F n x + G n x — defeq ✓ fine.\n\nThen the final: goal TendstoLocallyUniformlyOn (fun n x => dpsiSeqR n x) DinfR atTop (Ioi 0):\n```lean\n  have hdecomp : ∀ n : ℕ, (Set.Ioi 0).EqOn (dpsiSeqR n)\n      (fun x => (Real.log n - (harmonic n : ℝ)) + (-1 / x + ∑ m ∈ Finset.range n, dpsiTermR x m)) :=\n    fun n x _ => dpsiSeqR_eq n x\n  have hlimit : (Set.Ioi 0).EqOn\n      (fun x => -Real.eulerMascheroniConstant + (-1 / x + ∑' m : ℕ, dpsiTermR x m)) DinfR :=\n    fun x _ => by rw [DinfR]; ring\n  exact ((hA.add (hB.add hC)).congr hdecomp).congr_right hlimit\n```\nwith dpsiSeqR_eq n x : dpsiSeqR n x = (log n − ↑harmonic) + (−1/x + Σ ...) ✓ — so dpsiSeqR_eq's statement must have dpsiSeqR n x on the LEFT ✓ adjust.\n\nThe congr direction: TendstoLocallyUniformlyOn.congr (hf : ... F f) (hg : ∀ n, s.EqOn (F n) (G n)) : ... G f — I have the decomposed sequence converging (F := decomposed, G := dpsiSeqR): hg : ∀ n, EqOn (F n) (G n) — hdecomp gives dpsiSeqR n x = decomposed x — so EqOn (dpsiSeqR n) (decomposed n) — hmm — congr's hg : EqOn (F n) (G n) with F the PROVED convergence's sequence. Let me set: hAsum := (hA.add (hB.add hC)) : TendstoLocallyUniformlyOn DECOMPOSED... — then .congr (fun n x _ => (dpsiSeqR_eq n x).symm)?? — EqOn (DECOMPOSED n) (dpsiSeqR n) means ∀ x ∈ s, DECOMPOSED n x = dpsiSeqR n x — that's (dpsiSeqR_eq n x).symm ✓ so .congr (fun n x _ => (dpsiSeqR_eq n x).symm) : TendstoLocallyUniformlyOn dpsiSeqR (the decomposed limit) — then .congr_right hlimit with hlimit : EqOn (decomposed-limit) DinfR: ∀ x ∈ s, decomp-limit x = DinfR x — my hlimit's content: fun x => by rw [DinfR]; ring — the DinfR unfold: DinfR x := −γ − 1/x + tsum — the goal: −γ + (−1/x + tsum) = DinfR x — rw [DinfR] unfolds RHS → ... = −γ − 1/x + tsum — ring ✓ — hmm rw [DinfR] on the goal's RHS occurrence — DinfR is a def — rw [DinfR] uses its equation lemma DinfR.eq_def? For `def DinfR (x : ℝ) : ℝ := ...` the equation DinfR x = ... ✓ should work (or show/simp only [DinfR]).\n\nHmm — congr_right (hg : s.EqOn f g) : TendstoLocallyUniformlyOn F g — takes f = current limit, g = new limit — hg : EqOn f g — so hlimit : EqOn (decomp-limit) DinfR — content ∀ x ∈ s, decomp-limit x = DinfR x ✓ as I have it.\n\nNow also Section 2's hasDerivAt_of_tendstoLocallyUniformlyOn — its signature (from the earlier read): (hs : IsOpen s) (hf' : TendstoLocallyUniformlyOn f' g' l s) (hf : ∀ᶠ n in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x) (hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))) (hx : x ∈ s) : HasDerivAt g (g' x) x — with f : ι → 𝕜 → 𝕜 (n FIRST) ✓ matches my flipped dpsiSeqR. The f: fun n => fun x => BohrMollerup.logGammaSeq x n; f' := dpsiSeqR; g := Real.log ∘ Real.Gamma; g' := DinfR ✓.\n\nFor hfg: ∀ x ∈ Ioi 0, Tendsto (fun n => logGammaSeq x n) atTop (𝓝 ((Real.log ∘ Real.Gamma) x)) — from BohrMollerup.tendsto_log_gamma hx : Tendsto (logGammaSeq x) atTop (𝓝 (Real.log (Real.Gamma x))) — the target's (Real.log ∘ Real.Gamma) x — defeq Real.log (Real.Gamma x) ✓ exact or simpa.\n\nOK — let me now also double-check `summable_nat_add_iff`: `summable_nat_add_iff (k : ℕ) : Summable (fun n => f (n + k)) ↔ Summable f` ✓ exists (I'm confident).\n\nAnd the harmonic def — let me check quickly: `harmonic (n : ℕ) : ℚ := ∑ i ∈ Finset.range n, (↑(i + 1))⁻¹`? — hmm — actually from the first error output: `(↑(i + 1))⁻¹` — so the terms are (↑(i+1) : ℚ)⁻¹ ✓.\n\nLet me now rewrite the whole Section 2 correctly.","signature":""},{"type":"text","text":"Now rewriting Section 2 correctly (arg order flip, the sum_eq decomposition fixes, isMinOn/isMaxOn)."},{"type":"tool_use","id":"Edit_316","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean","old_string":"/-! ## 2. The deriv-limit interchange: (log Γ)' = DinfR on (0,∞) -/\n\n/-- The derivative of logGammaSeq x n in x: log n − Σ_{m=0}^n 1/(x+m). -/\ndef dpsiSeqR (x : ℝ) (n : ℕ) : ℝ :=\n  Real.log n - ∑ m ∈ Finset.range (n + 1), 1 / (x + m)\n\n/-- The derivative sequence decomposes as (log n − H_n) + (−1/x + partial series). -/\nlemma dpsiSeqR_eq (x : ℝ) (n : ℕ) :\n    dpsiSeqR x n = (Real.log n - (harmonic n : ℝ)) +\n      (-1 / x + ∑ m ∈ Finset.range n, dpsiTermR x m) := by\n  rw [dpsiSeqR]\n  have hh : (harmonic n : ℝ) = ∑ i ∈ Finset.range n, 1 / ((i : ℝ) + 1) := by\n    rw [harmonic, Nat.cast_sum]\n    apply Finset.sum_congr rfl\n    intro i hi\n    rw [Nat.cast_inv, Nat.cast_add, Nat.cast_one]\n  rw [hh]\n  have h2 : ∑ m ∈ Finset.range (n + 1), 1 / (x + (m : ℝ)) =\n      1 / x + ∑ i ∈ Finset.range n, 1 / (x + i + 1) := by\n    rw [Finset.sum_range_succ']  -- peels the m = 0 term: range (n+1) → range n + f 0 form\n    have e : ∀ i : ℕ, 1 / (x + (i + 1 : ℝ)) = 1 / (x + i + 1 : ℝ) := fun i => by push_cast; ring_nf\n    rw [Finset.sum_congr rfl (fun i _ => e i)]\n    ring\n  rw [h2]\n  have h3 : ∑ i ∈ Finset.range n, (1 / ((i : ℝ) + 1) - 1 / (x + i + 1)) =\n      ∑ i ∈ Finset.range n, dpsiTermR x i := by\n    apply Finset.sum_congr rfl\n    intro i hi\n    rw [dpsiTermR]\n    ring\n  rw [← Finset.sum_sub_distrib] at h3\n  rw [← h3]\n  ring\n\n/-- The series part converges uniformly on compacts inside (0,∞). -/\nlemma dpsiTermR_summableLocallyUniformlyOn :\n    SummableLocallyUniformlyOn (fun m : ℕ => fun x : ℝ => dpsiTermR x m) (Set.Ioi 0) := by\n  apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_Ioi\n  intro K hK hKc\n  obtain ⟨c, hcK, hc0⟩ := hKc.exists_sInf_mem (by\n    obtain ⟨x, hx⟩ := hK\n    exact ⟨x, hx⟩) -- sInf K ∈ K\n  obtain ⟨C, hCK, _⟩ := hKc.exists_sSup_mem (by\n    obtain ⟨x, hx⟩ := hK\n    exact ⟨x, hx⟩)\n  have hc0' : 0 < c := hK hcK  -- c ∈ K ⊆ Ioi 0\n  refine ⟨fun m => C / ((m : ℝ) + 1) ^ 2, summable_div_add_one_sq C, fun m => fun x hx => ?_⟩\n  have hx0 : 0 < x := hK hx\n  have hxc : c ≤ x := csInf_le (hKc.bddBelow) hx\n  have hxC : x ≤ C := le_csSup (hKc.bddAbove) hx\n  rw [Real.norm_eq_abs, abs_of_nonneg (dpsiTermR_nonneg hx0)]\n  calc dpsiTermR x m ≤ x / ((m : ℝ) + 1) ^ 2 := dpsiTermR_le hx0 m\n    _ ≤ C / ((m : ℝ) + 1) ^ 2 := by\n        apply (div_le_div_iff_of_pos_right (by positivity : (0 : ℝ) < ((m : ℝ) + 1) ^ 2)).mpr\n        exact hxC\n\n/-- The derivative sequence converges locally uniformly to DinfR on (0,∞). -/\nlemma dpsiSeqR_tendstoLocallyUniformlyOn :\n    TendstoLocallyUniformlyOn dpsiSeqR DinfR atTop (Set.Ioi 0) := by\n  have hA : TendstoLocallyUniformlyOn (fun n => fun _ : ℝ => Real.log n - (harmonic n : ℝ))\n      (fun _ => -Real.eulerMascheroniConstant) atTop (Set.Ioi 0) := by\n    -- constant in x: from the pointwise harmonic-sub-log limit\n    have h := Real.tendsto_harmonic_sub_log\n    have h2 : Tendsto (fun n : ℕ => Real.log n - (harmonic n : ℝ)) atTop\n        (𝓝 (-Real.eulerMascheroniConstant)) := by\n      have h3 : (fun n : ℕ => Real.log n - (harmonic n : ℝ)) =\n          fun n => -((harmonic n : ℝ) - Real.log n) := by\n        funext n; ring\n      rw [h2]\n      exact h.neg\n    rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi]\n    intro K hK hKc\n    rw [Metric.tendstoUniformlyOn_iff]\n    intro ε hε\n    rw [Metric.tendsto_atTop] at h2\n    obtain ⟨N, hN⟩ := h2 ε hε\n    refine ⟨N, fun n hn x hx => ?_⟩\n    simpa using hN n hn\n  have hB : TendstoLocallyUniformlyOn (fun _ => fun x : ℝ => -1 / x) (fun x => -1 / x)\n      atTop (Set.Ioi 0) := tendstoLocallyUniformlyOn_const\n  have hC : TendstoLocallyUniformlyOn (fun n => fun x : ℝ => ∑ m ∈ Finset.range n, dpsiTermR x m)\n      (fun x => ∑' m : ℕ, dpsiTermR x m) atTop (Set.Ioi 0) := by\n    obtain ⟨g, hg⟩ := dpsiTermR_summableLocallyUniformlyOn\n    apply (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).congr_right\n    intro t ht\n    exact (hg.tsum_eqOn ht).symm\n  have hsum := (hA.add (hB.add hC))\n  apply hsum.congr\n  intro n x hx\n  rw [dpsiSeqR_eq]\n  simp [Pi.add_apply]\n\n/-- (log Γ)'(x) = DinfR(x) for x > 0 — the interchange. -/\nlemma deriv_log_Gamma_real {x : ℝ} (hx : 0 < x) :\n    deriv (Real.log ∘ Real.Gamma) x = DinfR x := by\n  have hfg : ∀ y ∈ Set.Ioi 0, Tendsto (fun n => BohrMollerup.logGammaSeq y n) atTop\n      (𝓝 ((Real.log ∘ Real.Gamma) y)) := by\n    intro y hy\n    exact BohrMollerup.tendsto_log_gamma hy\n  have hf : ∀ᶠ n in atTop, ∀ y ∈ Set.Ioi 0,\n      HasDerivAt (fun y => BohrMollerup.logGammaSeq y n) (dpsiSeqR y n) y := by\n    apply Filter.Eventually.of_forall\n    intro n y hy\n    -- logGammaSeq y n = y log n + log n! − Σ_{m=0}^n log (y + m)\n    have h1 : HasDerivAt (fun y => y * Real.log n) (Real.log n) y := by\n      simpa using (hasDerivAt_id y).mul_const (Real.log n)\n    have h2 : HasDerivAt (fun _ : ℝ => Real.log (n !)) 0 y := hasDerivAt_const _ _\n    have h3 : HasDerivAt (fun y => ∑ m ∈ Finset.range (n + 1), Real.log (y + (m : ℝ)))\n        (∑ m ∈ Finset.range (n + 1), (1 / (y + (m : ℝ)))) y := by\n      apply HasDerivAt.sum\n      intro m hm\n      have hym : (0 : ℝ) < y + m := by\n        have := hy\n        rw [Set.mem_Ioi] at this\n        positivity\n      have h4 : HasDerivAt (fun y : ℝ => y + (m : ℝ)) 1 y := by\n        simpa using (hasDerivAt_id y).add_const (m : ℝ)\n      have h5 := (Real.hasDerivAt_log (ne_of_gt hym)).comp y h4\n      rw [mul_one] at h5\n      -- h5 : HasDerivAt (log ∘ (y + m)) ((y+m)⁻¹ * 1)... — normalize\n      have heq : (Real.log ∘ fun y : ℝ => y + (m : ℝ)) = fun y => Real.log (y + (m : ℝ)) := rfl\n      rw [heq] at h5\n      have hinv : (1 : ℝ) / (y + (m : ℝ)) = (y + (m : ℝ))⁻¹ := by rw [one_div]\n      rw [hinv]\n      exact h5\n    -- assemble: deriv (y log n + log n! − Σ log (y+m)) = log n − Σ 1/(y+m)\n    have hmain : HasDerivAt (fun y => y * Real.log n + Real.log (n !) -\n        ∑ m ∈ Finset.range (n + 1), Real.log (y + (m : ℝ)))\n        (Real.log n + 0 - ∑ m ∈ Finset.range (n + 1), 1 / (y + (m : ℝ))) y := by\n      exact (h1.add h2).sub h3\n    have hzero : Real.log n + 0 - ∑ m ∈ Finset.range (n + 1), 1 / (y + (m : ℝ)) = dpsiSeqR y n := by\n      rw [dpsiSeqR]\n      ring\n    rw [hzero] at hmain\n    have heq : (fun y => BohrMollerup.logGammaSeq y n) =\n        fun y => y * Real.log n + Real.log (n !) -\n          ∑ m ∈ Finset.range (n + 1), Real.log (y + (m : ℝ)) := by\n      funext y\n      rw [BohrMollerup.logGammaSeq]\n    rw [heq] at hmain\n    exact hmain\n  have h := hasDerivAt_of_tendstoLocallyUniformlyOn isOpen_Ioi dpsiSeqR_tendstoLocallyUniformlyOn\n    hf hfg (Set.mem_Ioi.mpr hx)\n  exact h.deriv\n\n/-- ψ_real(x) := Γ'(x)/Γ(x) = DinfR(x) for x > 0. -/\nlemma psiReal_eq_DinfR {x : ℝ} (hx : 0 < x) :\n    deriv Real.Gamma x / Real.Gamma x = DinfR x := by\n  have h := deriv_log_Gamma_real hx\n  have hG : DifferentiableAt ℝ Real.Gamma x := by\n    apply Real.differentiableAt_Gamma\n    intro m\n    intro hmeq\n    have : (0 : ℝ) < x := hx\n    rw [← hmeq] at this\n    have hm : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m\n    linarith\n  have hG0 : Real.Gamma x ≠ 0 := (Real.Gamma_pos_of_pos hx).ne'\n  have hchain : deriv (Real.log ∘ Real.Gamma) x = deriv Real.Gamma x / Real.Gamma x := by\n    have h1 : HasDerivAt Real.Gamma (deriv Real.Gamma x) x := hG.hasDerivAt\n    have h2 : HasDerivAt Real.log (1 / Real.Gamma x) (Real.Gamma x) :=\n      Real.hasDerivAt_log hG0\n    have h3 := h2.comp x h1\n    -- h3 : HasDerivAt (log ∘ Gamma) ((1/Gamma x) * Gamma' x) x\n    have heq : (Real.log ∘ Real.Gamma) = fun y => Real.log (Real.Gamma y) := rfl\n    rw [heq] at h3\n    rw [h3.deriv]\n    field_simp [hG0]\n  rw [hchain] at h\n  exact h\n\nend NguyenRH1","new_string":"/-! ## 2. The deriv-limit interchange: (log Γ)' = DinfR on (0,∞) -/\n\n/-- The derivative of logGammaSeq x n in x: log n − Σ_{m=0}^n 1/(x+m). -/\ndef dpsiSeqR (n : ℕ) (x : ℝ) : ℝ :=\n  Real.log n - ∑ m ∈ Finset.range (n + 1), 1 / (x + m)\n\n/-- The derivative sequence decomposes as (log n − H_n) + (−1/x + partial series). -/\nlemma dpsiSeqR_eq (n : ℕ) (x : ℝ) :\n    dpsiSeqR n x = (Real.log n - (harmonic n : ℝ)) +\n      (-1 / x + ∑ m ∈ Finset.range n, dpsiTermR x m) := by\n  rw [dpsiSeqR]\n  have hh : (harmonic n : ℝ) = ∑ i ∈ Finset.range n, 1 / ((i : ℝ) + 1) := by\n    rw [harmonic]\n    push_cast\n    apply Finset.sum_congr rfl\n    intro i hi\n    rw [one_div]\n  have h2 : ∑ m ∈ Finset.range (n + 1), 1 / (x + (m : ℝ)) =\n      1 / x + ∑ i ∈ Finset.range n, 1 / (x + i + 1) := by\n    rw [Finset.sum_range_succ']\n    have e : ∀ i : ℕ, 1 / (x + ((i + 1 : ℕ) : ℝ)) = 1 / (x + i + 1 : ℝ) := fun i => by\n      push_cast\n      ring_nf\n    rw [Finset.sum_congr rfl (fun i _ => e i)]\n    have e0 : (fun m => 1 / (x + (m : ℝ))) 0 = 1 / x := by simp\n    rw [e0]\n    ring\n  have h3 : ∑ i ∈ Finset.range n, dpsiTermR x i =\n      ∑ i ∈ Finset.range n, 1 / ((i : ℝ) + 1) - ∑ i ∈ Finset.range n, 1 / (x + i + 1) := by\n    rw [← Finset.sum_sub_distrib]\n    apply Finset.sum_congr rfl\n    intro i hi\n    rw [dpsiTermR]\n  rw [hh, h2, h3]\n  ring\n\n/-- The series part converges uniformly on compacts inside (0,∞). -/\nlemma dpsiTermR_summableLocallyUniformlyOn :\n    SummableLocallyUniformlyOn (fun m : ℕ => fun x : ℝ => dpsiTermR x m) (Set.Ioi 0) := by\n  apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_Ioi\n  intro K hK hKc\n  by_cases hKe : K = ∅\n  · subst hKe\n    exact ⟨0, summable_zero, fun m x hx => by simp at hx⟩\n  · obtain ⟨x0, hx0⟩ := Set.nonempty_iff_ne_empty.mpr hKe\n    obtain ⟨c, hcK, hcle⟩ := hKc.exists_isMinOn ⟨x0, hx0⟩ (continuous_id.continuousOn)\n    obtain ⟨C, hCK, hCle⟩ := hKc.exists_isMaxOn ⟨x0, hx0⟩ (continuous_id.continuousOn)\n    have hc0 : 0 < c := hK hcK\n    refine ⟨fun m => C / ((m : ℝ) + 1) ^ 2, summable_div_add_one_sq C, fun m x hx => ?_⟩\n    have hx0 : 0 < x := hK hx\n    have hxC : x ≤ C := hCle x hx\n    rw [Real.norm_eq_abs, abs_of_nonneg (dpsiTermR_nonneg hx0)]\n    calc dpsiTermR x m ≤ x / ((m : ℝ) + 1) ^ 2 := dpsiTermR_le hx0 m\n      _ ≤ C / ((m : ℝ) + 1) ^ 2 :=\n          (div_le_div_iff_of_pos_right (by positivity : (0 : ℝ) < ((m : ℝ) + 1) ^ 2)).mpr hxC\n\n/-- The derivative sequence converges locally uniformly to DinfR on (0,∞). -/\nlemma dpsiSeqR_tendstoLocallyUniformlyOn :\n    TendstoLocallyUniformlyOn dpsiSeqR DinfR atTop (Set.Ioi 0) := by\n  have hA : TendstoLocallyUniformlyOn (fun n => fun _ : ℝ => Real.log n - (harmonic n : ℝ))\n      (fun _ => -Real.eulerMascheroniConstant) atTop (Set.Ioi 0) := by\n    have h := Real.tendsto_harmonic_sub_log\n    have h2 : Tendsto (fun n : ℕ => Real.log n - (harmonic n : ℝ)) atTop\n        (𝓝 (-Real.eulerMascheroniConstant)) := by\n      have h3 : (fun n : ℕ => Real.log n - (harmonic n : ℝ)) =\n          fun n => -((harmonic n : ℝ) - Real.log n) := by\n        funext n; ring\n      rw [h3]\n      exact h.neg\n    rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi]\n    intro K hK hKc\n    rw [Metric.tendstoUniformlyOn_iff]\n    intro ε hε\n    rw [Metric.tendsto_atTop] at h2\n    obtain ⟨N, hN⟩ := h2 ε hε\n    rw [Filter.eventually_atTop]\n    exact ⟨N, fun n hn x hx => by simpa using hN n hn⟩\n  have hB : TendstoLocallyUniformlyOn (fun _ : ℕ => fun x : ℝ => -1 / x) (fun x => -1 / x)\n      atTop (Set.Ioi 0) := by\n    rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi]\n    intro K hK hKc\n    rw [Metric.tendstoUniformlyOn_iff]\n    intro ε hε\n    rw [Filter.eventually_atTop]\n    exact ⟨0, fun n _ x _ => by simpa using hε⟩\n  have hC : TendstoLocallyUniformlyOn (fun n => fun x : ℝ => ∑ m ∈ Finset.range n, dpsiTermR x m)\n      (fun x => ∑' m : ℕ, dpsiTermR x m) atTop (Set.Ioi 0) := by\n    obtain ⟨g, hg⟩ := dpsiTermR_summableLocallyUniformlyOn\n    apply (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).congr_right\n    intro t ht\n    exact (hg.tsum_eqOn ht).symm\n  have hdecomp : ∀ n : ℕ, (Set.Ioi 0).EqOn (dpsiSeqR n)\n      (fun x => (Real.log n - (harmonic n : ℝ)) +\n        (-1 / x + ∑ m ∈ Finset.range n, dpsiTermR x m)) :=\n    fun n x _ => dpsiSeqR_eq n x\n  have hlimit : (Set.Ioi 0).EqOn\n      (fun x => -Real.eulerMascheroniConstant + (-1 / x + ∑' m : ℕ, dpsiTermR x m)) DinfR :=\n    fun x _ => by rw [DinfR]; ring\n  exact ((hA.add (hB.add hC)).congr (fun n x _ => (dpsiSeqR_eq n x).symm)).congr_right hlimit\n\n/-- (log Γ)'(x) = DinfR(x) for x > 0 — the interchange. -/\nlemma deriv_log_Gamma_real {x : ℝ} (hx : 0 < x) :\n    deriv (Real.log ∘ Real.Gamma) x = DinfR x := by\n  have hfg : ∀ y ∈ Set.Ioi 0, Tendsto (fun n => BohrMollerup.logGammaSeq y n) atTop\n      (𝓝 ((Real.log ∘ Real.Gamma) y)) := by\n    intro y hy\n    exact BohrMollerup.tendsto_log_gamma hy\n  have hf : ∀ᶠ n in atTop, ∀ y ∈ Set.Ioi 0,\n      HasDerivAt (fun y => BohrMollerup.logGammaSeq y n) (dpsiSeqR n y) y := by\n    apply Filter.Eventually.of_forall\n    intro n y hy\n    have h1 : HasDerivAt (fun y => y * Real.log n) (Real.log n) y := by\n      simpa using (hasDerivAt_id y).mul_const (Real.log n)\n    have h2 : HasDerivAt (fun _ : ℝ => Real.log (n !)) 0 y := hasDerivAt_const _ _\n    have h3 : HasDerivAt (fun y => ∑ m ∈ Finset.range (n + 1), Real.log (y + (m : ℝ)))\n        (∑ m ∈ Finset.range (n + 1), (1 / (y + (m : ℝ)))) y := by\n      apply HasDerivAt.sum\n      intro m hm\n      have hym : (0 : ℝ) < y + m := by\n        have := hy\n        rw [Set.mem_Ioi] at this\n        positivity\n      have h4 : HasDerivAt (fun y : ℝ => y + (m : ℝ)) 1 y := by\n        simpa using (hasDerivAt_id y).add_const (m : ℝ)\n      have h5 := (Real.hasDerivAt_log (ne_of_gt hym)).comp y h4\n      rw [mul_one] at h5\n      have heq : (Real.log ∘ fun y : ℝ => y + (m : ℝ)) = fun y => Real.log (y + (m : ℝ)) := rfl\n      rw [heq] at h5\n      have hinv : (1 : ℝ) / (y + (m : ℝ)) = (y + (m : ℝ))⁻¹ := by rw [one_div]\n      rw [hinv]\n      exact h5\n    have hmain : HasDerivAt (fun y => y * Real.log n + Real.log (n !) -\n        ∑ m ∈ Finset.range (n + 1), Real.log (y + (m : ℝ)))\n        (Real.log n + 0 - ∑ m ∈ Finset.range (n + 1), 1 / (y + (m : ℝ))) y :=\n      (h1.add h2).sub h3\n    have hzero : Real.log n + 0 - ∑ m ∈ Finset.range (n + 1), 1 / (y + (m : ℝ)) =\n        dpsiSeqR n y := by\n      rw [dpsiSeqR]\n      ring\n    rw [hzero] at hmain\n    have heq : (fun y => BohrMollerup.logGammaSeq y n) =\n        fun y => y * Real.log n + Real.log (n !) -\n          ∑ m ∈ Finset.range (n + 1), Real.log (y + (m : ℝ)) := by\n      funext y\n      rw [BohrMollerup.logGammaSeq]\n    rw [heq] at hmain\n    exact hmain\n  have h := hasDerivAt_of_tendstoLocallyUniformlyOn isOpen_Ioi dpsiSeqR_tendstoLocallyUniformlyOn\n    hf hfg (Set.mem_Ioi.mpr hx)\n  exact h.deriv\n\n/-- ψ_real(x) := Γ'(x)/Γ(x) = DinfR(x) for x > 0. -/\nlemma psiReal_eq_DinfR {x : ℝ} (hx : 0 < x) :\n    deriv Real.Gamma x / Real.Gamma x = DinfR x := by\n  have h := deriv_log_Gamma_real hx\n  have hG : DifferentiableAt ℝ Real.Gamma x := by\n    apply Real.differentiableAt_Gamma\n    intro m hmeq\n    have hxx : (0 : ℝ) < x := hx\n    rw [← hmeq] at hxx\n    have hm : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m\n    linarith\n  have hG0 : Real.Gamma x ≠ 0 := (Real.Gamma_pos_of_pos hx).ne'\n  have hchain : deriv (Real.log ∘ Real.Gamma) x = deriv Real.Gamma x / Real.Gamma x := by\n    have h1 : HasDerivAt Real.Gamma (deriv Real.Gamma x) x := hG.hasDerivAt\n    have h2 : HasDerivAt Real.log (1 / Real.Gamma x) (Real.Gamma x) :=\n      Real.hasDerivAt_log hG0\n    have h3 := h2.comp x h1\n    have heq : (Real.log ∘ Real.Gamma) = fun y => Real.log (Real.Gamma y) := rfl\n    rw [heq] at h3\n    rw [h3.deriv]\n    field_simp [hG0]\n  rw [hchain] at h\n  exact h\n\nend NguyenRH1"},"extra_content":null}]