Commit 2023-01-26 08:02 0ee3e6f5

View on Github →

feat(analysis/special_functions/gamma): monotonicity of the Gamma function (#18246) Show (using the log-convexity results proved in #18188) that Gamma is strictly increasing for 2 ≤ x.

Estimated changes

Modified src/analysis/convex/function.lean

added theorem concave_on.left_lt_of_lt_right'

added theorem concave_on.left_lt_of_lt_right

added theorem concave_on.lt_right_of_left_lt'

added theorem concave_on.lt_right_of_left_lt

added theorem convex_on.lt_left_of_right_lt'

added theorem convex_on.lt_left_of_right_lt

added theorem convex_on.lt_right_of_left_lt'

added theorem convex_on.lt_right_of_left_lt

deleted theorem strict_concave_on.left_lt_of_lt_right'

deleted theorem strict_concave_on.left_lt_of_lt_right

deleted theorem strict_concave_on.lt_right_of_left_lt'

deleted theorem strict_concave_on.lt_right_of_left_lt

deleted theorem strict_convex_on.lt_left_of_right_lt'

deleted theorem strict_convex_on.lt_left_of_right_lt

deleted theorem strict_convex_on.lt_right_of_left_lt'

deleted theorem strict_convex_on.lt_right_of_left_lt

Modified src/analysis/convex/slope.lean

added theorem convex_on.strict_mono_of_lt

Modified src/analysis/special_functions/gamma.lean

added theorem complex.Gamma_conj

added theorem complex.Gamma_integral_conj

added theorem complex.Gamma_of_real

added theorem real.Gamma_strict_mono_on_Ici

added theorem real.Gamma_three_div_two_lt_one

added theorem real.Gamma_two

added theorem real.convex_on_Gamma

Modified src/analysis/special_functions/gaussian.lean

modified theorem complex.Gamma_one_half_eq

added theorem real.Gamma_one_half_eq