From 56384073134865451000698b8c377af8a8f542a5 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Mon, 20 Apr 2026 14:26:18 +0800 Subject: [PATCH 1/2] refactor(Analysis): golf Gamma Basic --- .../Analysis/SpecialFunctions/Gamma/Basic.lean | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean index 14d25fb22eb80f..77e13d24a2726b 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean @@ -408,18 +408,8 @@ def Gamma (s : ℝ) : ℝ := set_option backward.isDefEq.respectTransparency false in theorem Gamma_eq_integral {s : ℝ} (hs : 0 < s) : Gamma s = ∫ x in Ioi 0, exp (-x) * x ^ (s - 1) := by - rw [Gamma, Complex.Gamma_eq_integral (by rwa [Complex.ofReal_re] : 0 < Complex.re s)] - dsimp only [Complex.GammaIntegral] - simp_rw [← Complex.ofReal_one, ← Complex.ofReal_sub] - suffices ∫ x : ℝ in Ioi 0, ↑(exp (-x)) * (x : ℂ) ^ ((s - 1 : ℝ) : ℂ) = - ∫ x : ℝ in Ioi 0, ((exp (-x) * x ^ (s - 1) : ℝ) : ℂ) by - have cc : ∀ r : ℝ, Complex.ofReal r = @RCLike.ofReal ℂ _ r := fun r => rfl - conv_lhs => rw [this]; enter [1, 2, x]; rw [cc] - rw [_root_.integral_ofReal, ← cc, Complex.ofReal_re] - refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_ - push_cast - rw [Complex.ofReal_cpow (le_of_lt hx)] - push_cast; rfl + rw [Gamma, Complex.Gamma_eq_integral (RCLike.ofReal_pos.mp hs), Complex.GammaIntegral_ofReal, + Complex.ofReal_re] theorem Gamma_add_one {s : ℝ} (hs : s ≠ 0) : Gamma (s + 1) = s * Gamma s := by simp_rw [Gamma] @@ -521,7 +511,7 @@ theorem Gamma_ne_zero {s : ℝ} (hs : ∀ m : ℕ, s ≠ -m) : Gamma s ≠ 0 := apply n_ih · intro m specialize hs (1 + m) - contrapose hs + contrapose! hs rw [← eq_sub_iff_add_eq] at hs rw [hs] push_cast From 99d79081202ca3f3e77182aaba324a99480ec6e1 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 20 Apr 2026 14:28:57 +0800 Subject: [PATCH 2/2] Update Basic.lean --- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean index 77e13d24a2726b..0b1a921be8277a 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean @@ -511,7 +511,7 @@ theorem Gamma_ne_zero {s : ℝ} (hs : ∀ m : ℕ, s ≠ -m) : Gamma s ≠ 0 := apply n_ih · intro m specialize hs (1 + m) - contrapose! hs + contrapose hs rw [← eq_sub_iff_add_eq] at hs rw [hs] push_cast