Commit 2024-12-02 01:32 dde4f2ec

View on Github →

feat: an equality condition for AM-GM inequality (#19435) Add some theorems on the equality condition of the weighted AM-GM inequality for real-valued nonnegative functions, referring to geom_mean_arith_mean_weighted_eq_iff in Mathlib/Analysis/MeanInequalities.lean.

Estimated changes

Modified Mathlib/Analysis/MeanInequalities.lean

added theorem Real.geom_mean_eq_arith_mean_weighted_iff'

added theorem Real.geom_mean_eq_arith_mean_weighted_iff

added theorem Real.geom_mean_lt_arith_mean_weighted_iff_of_pos