Mean value inequalities #
In this file we prove several mean inequalities for finite sums. Versions for integrals of some of
these inequalities are available in MeasureTheory.MeanInequalities
.
Main theorems: generalized mean inequality #
The inequality says that for two non-negative vectors
Currently we only prove this inequality for Mathlib
, we provide
different theorems for natural exponents (pow_arith_mean_le_arith_mean_pow
), integer exponents
(zpow_arith_mean_le_arith_mean_zpow
), and real exponents (rpow_arith_mean_le_arith_mean_rpow
and
arith_mean_le_rpow_mean
). In the first two cases we prove
TODO #
- each inequality
A ≤ B
should come with a theoremA = B ↔ _
; one of the ways to prove them is to defineStrictConvexOn
functions. - generalized mean inequality with any
p ≤ q
, including negative numbers; - prove that the power mean tends to the geometric mean as the exponent tends to zero.