Commit 2024-07-26 19:28 466a8e2e

View on Github →

chore(BohrMollerup): move convexity lemmas to Analysis.Convex.Function (#15031) Addresses a porting TODO

Estimated changes

Modified Mathlib/Analysis/Convex/Function.lean

added theorem ConcaveOn.add_const

added theorem ConcaveOn.congr

added theorem ConvexOn.add_const

added theorem ConvexOn.congr

added theorem StrictConcaveOn.add_const

added theorem StrictConcaveOn.congr

added theorem StrictConvexOn.add_const

added theorem StrictConvexOn.congr

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

deleted theorem ConcaveOn.add_const

deleted theorem ConcaveOn.congr

deleted theorem ConvexOn.add_const

deleted theorem ConvexOn.congr

deleted theorem StrictConcaveOn.add_const

deleted theorem StrictConcaveOn.congr

deleted theorem StrictConvexOn.add_const

deleted theorem StrictConvexOn.congr