Commit 2023-06-14 11:40 d275e65b

View on Github →

feat: port Analysis.SpecialFunctions.Gamma.Basic (#5042)

Estimated changes

Modified Mathlib.lean

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

added def Complex.Gamma

added theorem Complex.GammaAux_recurrence1

added theorem Complex.GammaAux_recurrence2

added def Complex.GammaIntegral

added theorem Complex.GammaIntegral_add_one

added theorem Complex.GammaIntegral_conj

added theorem Complex.GammaIntegral_convergent

added theorem Complex.GammaIntegral_eq_mellin

added theorem Complex.GammaIntegral_ofReal

added theorem Complex.GammaIntegral_one

added theorem Complex.Gamma_add_one

added theorem Complex.Gamma_conj

added theorem Complex.Gamma_eq_GammaAux

added theorem Complex.Gamma_eq_integral

added theorem Complex.Gamma_nat_eq_factorial

added theorem Complex.Gamma_neg_nat_eq_zero

added theorem Complex.Gamma_ofReal

added theorem Complex.Gamma_one

added theorem Complex.Gamma_zero

added theorem Complex.differentiableAt_Gamma

added theorem Complex.differentiableAt_GammaAux

added theorem Complex.hasDerivAt_GammaIntegral

added def Complex.partialGamma

added theorem Complex.partialGamma_add_one

added theorem Complex.tendsto_partialGamma

added theorem Complex.tendsto_self_mul_Gamma_nhds_zero

added def Real.Gamma

added theorem Real.GammaIntegral_convergent

added theorem Real.Gamma_add_one

added theorem Real.Gamma_eq_integral

added theorem Real.Gamma_eq_zero_iff

added theorem Real.Gamma_integrand_isLittleO

added theorem Real.Gamma_nat_eq_factorial

added theorem Real.Gamma_ne_zero

added theorem Real.Gamma_neg_nat_eq_zero

added theorem Real.Gamma_one

added theorem Real.Gamma_pos_of_pos

added theorem Real.Gamma_zero

added theorem Real.differentiableAt_Gamma