Mean value inequalities #
In this file we prove several inequalities for finite sums, including AM-GM inequality,
HM-GM inequality, Young's inequality, Hölder inequality, and Minkowski inequality. Versions for
integrals of some of these inequalities are available in MeasureTheory.MeanInequalities
.
Main theorems #
AM-GM inequality: #
The inequality says that the geometric mean of a tuple of non-negative numbers is less than or equal
to their arithmetic mean. We prove the weighted version of this inequality: if
We prove a few versions of this inequality. Each of the following lemmas comes in two versions:
a version for real-valued non-negative functions is in the Real
namespace, and a version for
NNReal
-valued functions is in the NNReal
namespace.
geom_mean_le_arith_mean_weighted
: weighted version for functions onFinset
s;geom_mean_le_arith_mean2_weighted
: weighted version for two numbers;geom_mean_le_arith_mean3_weighted
: weighted version for three numbers;geom_mean_le_arith_mean4_weighted
: weighted version for four numbers.
HM-GM inequality: #
The inequality says that the harmonic mean of a tuple of positive numbers is less than or equal
to their geometric mean. We prove the weighted version of this inequality: if
The inequalities are proven only for real valued positive functions on Finset
s, and namespaced in
Real
. The weighted version follows as a corollary of the weighted AM-GM inequality.
Young's inequality #
Young's inequality says that for non-negative numbers a
, b
, p
, q
such that
This inequality is a special case of the AM-GM inequality. It is then used to prove Hölder's inequality (see below).
Hölder's inequality #
The inequality says that for two conjugate exponents p
and q
(i.e., for two positive numbers
such that
We give versions of this result in ℝ
, ℝ≥0
and ℝ≥0∞
.
There are at least two short proofs of this inequality. In our proof we prenormalize both vectors,
then apply Young's inequality to each
Minkowski's inequality #
The inequality says that for p ≥ 1
the function
We give versions of this result in Real
, ℝ≥0
and ℝ≥0∞
.
We deduce this inequality from Hölder's inequality. Namely, Hölder inequality implies that b
such that
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.
AM-GM inequality #
AM-GM inequality: The geometric mean is less than or equal to the arithmetic mean, weighted version for real-valued nonnegative functions.
HM-GM inequality #
HM-GM inequality: The harmonic mean is less than or equal to the geometric mean, weighted version for real-valued nonnegative functions.
Young's inequality #
Young's inequality, ℝ≥0∞
version with real conjugate exponents.
Hölder's and Minkowski's inequalities #
Hölder inequality: The scalar product of two functions is bounded by the product of their
L^p
and L^q
norms when p
and q
are conjugate exponents. Version for sums over finite sets,
with ℝ≥0
-valued functions.
Hölder inequality: the scalar product of two functions is bounded by the product of their
L^p
and L^q
norms when p
and q
are conjugate exponents. A version for NNReal
-valued
functions. For an alternative version, convenient if the infinite sums are already expressed as
p
-th powers, see inner_le_Lp_mul_Lq_hasSum
.
Hölder inequality: the scalar product of two functions is bounded by the product of their
L^p
and L^q
norms when p
and q
are conjugate exponents. A version for NNReal
-valued
functions. For an alternative version, convenient if the infinite sums are not already expressed as
p
-th powers, see inner_le_Lp_mul_Lq_tsum
.
The L_p
seminorm of a vector f
is the greatest value of the inner product
∑ i ∈ s, f i * g i
over functions g
of L_q
seminorm less than or equal to one.
Minkowski inequality: the L_p
seminorm of the infinite sum of two vectors is less than or
equal to the infinite sum of the L_p
-seminorms of the summands, if these infinite sums both
exist. A version for NNReal
-valued functions. For an alternative version, convenient if the
infinite sums are already expressed as p
-th powers, see Lp_add_le_hasSum_of_nonneg
.
Minkowski inequality: the L_p
seminorm of the infinite sum of two vectors is less than or
equal to the infinite sum of the L_p
-seminorms of the summands, if these infinite sums both
exist. A version for NNReal
-valued functions. For an alternative version, convenient if the
infinite sums are not already expressed as p
-th powers, see Lp_add_le_tsum_of_nonneg
.
Hölder inequality: the scalar product of two functions is bounded by the product of their
L^p
and L^q
norms when p
and q
are conjugate exponents. Version for sums over finite sets,
with real-valued functions.
Hölder inequality: the scalar product of two functions is bounded by the product of their
L^p
and L^q
norms when p
and q
are conjugate exponents. Version for sums over finite sets,
with real-valued nonnegative functions.
Weighted Hölder inequality in terms of Finset.expect
.
Hölder inequality: the scalar product of two functions is bounded by the product of their
L^p
and L^q
norms when p
and q
are conjugate exponents. A version for ℝ
-valued functions.
For an alternative version, convenient if the infinite sums are already expressed as p
-th powers,
see inner_le_Lp_mul_Lq_hasSum_of_nonneg
.
Hölder inequality: the scalar product of two functions is bounded by the product of their
L^p
and L^q
norms when p
and q
are conjugate exponents. A version for NNReal
-valued
functions. For an alternative version, convenient if the infinite sums are not already expressed as
p
-th powers, see inner_le_Lp_mul_Lq_tsum_of_nonneg
.
For 1 ≤ p
, the p
-th power of the sum of f i
is bounded above by a constant times the
sum of the p
-th powers of f i
. Version for sums over finite sets, with nonnegative ℝ
-valued
functions.
Minkowski inequality: the L_p
seminorm of the sum of two vectors is less than or equal
to the sum of the L_p
-seminorms of the summands. A version for ℝ
-valued nonnegative
functions.
Minkowski inequality: the L_p
seminorm of the infinite sum of two vectors is less than or
equal to the infinite sum of the L_p
-seminorms of the summands, if these infinite sums both
exist. A version for ℝ
-valued functions. For an alternative version, convenient if the infinite
sums are already expressed as p
-th powers, see Lp_add_le_hasSum_of_nonneg
.
Minkowski inequality: the L_p
seminorm of the infinite sum of two vectors is less than or
equal to the infinite sum of the L_p
-seminorms of the summands, if these infinite sums both
exist. A version for ℝ
-valued functions. For an alternative version, convenient if the infinite
sums are not already expressed as p
-th powers, see Lp_add_le_tsum_of_nonneg
.
Hölder inequality: the scalar product of two functions is bounded by the product of their
L^p
and L^q
norms when p
and q
are conjugate exponents. Version for sums over finite sets,
with ℝ≥0∞
-valued functions.