Commit 2024-10-17 04:14 8e52ebf8

View on Github →

chore: move differentiability of Gamma to a new file (#17775)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/MellinInversion.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

deleted theorem Complex.GammaIntegral_eq_mellin

deleted theorem Complex.differentiableAt_Gamma

deleted theorem Complex.differentiableAt_GammaAux

deleted theorem Complex.hasDerivAt_GammaIntegral

deleted theorem Complex.tendsto_self_mul_Gamma_nhds_zero

deleted theorem Real.differentiableAt_Gamma

Modified Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean

Created Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean

added theorem Complex.GammaIntegral_eq_mellin

added theorem Complex.differentiableAt_Gamma

added theorem Complex.differentiableAt_GammaAux

added theorem Complex.hasDerivAt_GammaIntegral

added theorem Complex.tendsto_self_mul_Gamma_nhds_zero

added theorem Real.differentiableAt_Gamma