Commit 2024-03-25 20:19 2c429c3c

View on Github →

feat: Bernoulli's inequality for 0 < p < 1 (#10982) Also substantially speed up some existing proofs in the p < 1 case.

Estimated changes

Modified Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean

modified theorem convexOn_rpow

added theorem rpow_one_add_le_one_add_mul_self

added theorem rpow_one_add_lt_one_add_mul_self

modified theorem strictConvexOn_rpow

Modified Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean