Commit 2023-06-26 14:58 3aedc708

View on Github →

feat: port Analysis.SpecialFunctions.Gamma.BohrMollerup (#5486)

Estimated changes

Modified Mathlib.lean

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

added theorem ConcaveOn.add_const

added theorem ConcaveOn.congr

added theorem ConvexOn.add_const

added theorem ConvexOn.congr

added theorem Real.BohrMollerup.f_add_nat_eq

added theorem Real.BohrMollerup.f_add_nat_ge

added theorem Real.BohrMollerup.f_add_nat_le

added theorem Real.BohrMollerup.f_nat_eq

added theorem Real.BohrMollerup.ge_logGammaSeq

added theorem Real.BohrMollerup.le_logGammaSeq

added def Real.BohrMollerup.logGammaSeq

added theorem Real.BohrMollerup.logGammaSeq_add_one

added theorem Real.BohrMollerup.tendsto_logGammaSeq

added theorem Real.BohrMollerup.tendsto_logGammaSeq_of_le_one

added theorem Real.BohrMollerup.tendsto_log_gamma

added theorem Real.Gamma_mul_Gamma_add_half_of_pos

added theorem Real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma

added theorem Real.Gamma_strictMonoOn_Ici

added theorem Real.Gamma_three_div_two_lt_one

added theorem Real.Gamma_two

added theorem Real.convexOn_Gamma

added theorem Real.convexOn_log_Gamma

added def Real.doublingGamma

added theorem Real.doublingGamma_add_one

added theorem Real.doublingGamma_eq_Gamma

added theorem Real.doublingGamma_log_convex_Ioi

added theorem Real.doublingGamma_one

added theorem Real.eq_Gamma_of_log_convex

added theorem Real.log_doublingGamma_eq

added theorem StrictConcaveOn.add_const

added theorem StrictConcaveOn.congr

added theorem StrictConvexOn.add_const

added theorem StrictConvexOn.congr