ENNReal.young_inequality
theorem ENNReal.young_inequality :
∀ (a b : ENNReal) {p q : ℝ}, p.IsConjExponent q → a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q := by
sorry
This is a version of Young's Inequality for extended nonnegative real numbers (`ENNReal`). It states that for all `a` and `b` in `ENNReal`, and any real numbers `p` and `q` that are conjugate exponents (meaning they satisfy the relationship $1/p + 1/q = 1$), the inequality `a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q` holds. In essence, this inequality provides an upper bound on the product of two extended nonnegative real numbers in terms of their powers and their conjugate exponents.
More concisely: For all `a` and `b` in `ENNReal` and real numbers `p` and `q` satisfying $1/p + 1/q = 1$, the inequality `a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q` holds.
|
Real.Lp_add_le_tsum_of_nonneg
theorem Real.Lp_add_le_tsum_of_nonneg :
∀ {ι : Type u} {f g : ι → ℝ} {p : ℝ},
1 ≤ p →
(∀ (i : ι), 0 ≤ f i) →
(∀ (i : ι), 0 ≤ g i) →
(Summable fun i => f i ^ p) →
(Summable fun i => g i ^ p) →
(Summable fun i => (f i + g i) ^ p) ∧
(∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤
(∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
The **Minkowski inequality** states that for any real number `p` greater than or equal to 1, and any two real-valued functions `f` and `g` defined on an index set `ι` such that each function value is nonnegative, if the infinite sums of `p`-th powers of `f` and `g` are both defined (summable), then the infinite sum of the `p`-th power of (`f(i)` + `g(i)`) is also defined. Moreover, the `p`-th root of this sum is less than or equal to the `p`-th root of the sum of `p`-th powers of `f(i)` plus the `p`-th root of the sum of `p`-th powers of `g(i)`. In mathematical notation, this can be written as $\left(\sum (f(i) + g(i))^p\right)^{1/p} \leq \left(\sum f(i)^p\right)^{1/p} + \left(\sum g(i)^p\right)^{1/p}$.
More concisely: For any real number `p` ≥ 1 and real-valued functions `f` and `g` on an index set `ι` with nonnegative values and summable `p`-th powers, the `p`-th root of the sum of `p`-th powers of `(f(i) + g(i))` is less than or equal to the `p`-th root of the sum of `p`-th powers of `f(i)` plus the `p`-th root of the sum of `p`-th powers of `g(i)`. In mathematical notation, $(\sum (f(i)+g(i))^p)^{1/p} \leq (\sum f(i)^p)^{1/p} + (\sum g(i)^p)^{1/p}$.
|
Real.geom_mean_le_arith_mean
theorem Real.geom_mean_le_arith_mean :
∀ {ι : Type u_1} (s : Finset ι) (w z : ι → ℝ),
(∀ i ∈ s, 0 ≤ w i) →
(0 < s.sum fun i => w i) →
(∀ i ∈ s, 0 ≤ z i) →
(s.prod fun i => z i ^ w i) ^ (s.sum fun i => w i)⁻¹ ≤ (s.sum fun i => w i * z i) / s.sum fun i => w i
This is the arithmetic mean-geometric mean (AM-GM) inequality theorem for real numbers. It states that for any finite set 's' of an arbitrary type 'ι', and any two functions 'w' and 'z' from 'ι' to the set of real numbers, if all of 'w i' are non-negative, the sum of 'w i' is positive, and all of 'z i' are non-negative, then the geometric mean of all 'z i' weighted by 'w i' is less than or equal to their arithmetic mean. The geometric mean is calculated by taking the product of each 'z i' raised to the power of 'w i' and then taking the inverse of the sum of 'w i' as the root. The arithmetic mean is calculated by summing the product of 'w i' and 'z i' and dividing by the sum of 'w i'.
More concisely: For any finite set of non-negative real numbers 'wi' and 'zn' with positive sum, the weighted geometric mean of 'zn' is less than or equal to the weighted arithmetic mean: (∏ i in I wi * zi ^ wi) ^ (1/∑ i in I wi) ≤ (∑ i in I wi * zi) / (∑ i in I wi).
|
ENNReal.Lp_add_le
theorem ENNReal.Lp_add_le :
∀ {ι : Type u} (s : Finset ι) (f g : ι → ENNReal) {p : ℝ},
1 ≤ p →
(s.sum fun i => (f i + g i) ^ p) ^ (1 / p) ≤
(s.sum fun i => f i ^ p) ^ (1 / p) + (s.sum fun i => g i ^ p) ^ (1 / p)
The theorem named "ENNReal.Lp_add_le" is a version of the Minkowski inequality for nonnegative functions valued in the extended nonnegative real numbers (usually denoted as [0, ∞]). It states that for any type `ι`, any finite set `s` of `ι`, any two functions `f` and `g` from `ι` to the extended nonnegative real numbers, and any real number `p` that is greater than or equal to 1, the `L_p` seminorm (defined as the p-th root of the sum of the p-th powers of the function values) of the sum of `f` and `g` is less than or equal to the sum of the `L_p` seminorms of `f` and `g`. In mathematical terms, this can be written as
\[
\left(\sum_{i\in s}(f(i) + g(i))^p\right)^{1/p} \leq \left(\sum_{i\in s} f(i)^p\right)^{1/p} + \left(\sum_{i\in s} g(i)^p\right)^{1/p}
\]
where ∑ denotes summation over the set `s`.
More concisely: For any finite set `s`, functions `f` and `g` from `ι` to the extended nonnegative real numbers, and real number `p ≥ 1`, the `L_p` seminorm of `f + g` is less than or equal to the sum of the `L_p` seminorms of `f` and `g`.
|
Real.rpow_sum_le_const_mul_sum_rpow
theorem Real.rpow_sum_le_const_mul_sum_rpow :
∀ {ι : Type u} (s : Finset ι) (f : ι → ℝ) {p : ℝ},
1 ≤ p → (s.sum fun i => |f i|) ^ p ≤ ↑s.card ^ (p - 1) * s.sum fun i => |f i| ^ p
The theorem states that for any real number `p` greater than or equal to 1, the `p`-th power of the sum of the absolute values of a function `f` applied to elements of a finite set `s` is less than or equal to the number of elements in `s` raised to the power `p - 1` times the sum of the `p`-th powers of the absolute values of `f` applied to elements of `s`. This is a version specific to finite sets with real-valued functions.
More concisely: For any real number `p` ≥ 1 and finite set `s` with real-valued function `f`, the sum of the absolute values of `f` applied to elements of `s` raised to the power `p` is less than or equal to the number of elements in `s` raised to the power `p - 1` times the sum of the `p`-th powers of the absolute values of `f` applied to elements of `s`. In symbols: ∑ₙ (|f(xₙ)|^p) ≤ |s|^(p-1) * ∑ₙ (|f(xₙ)|^p), where the summation runs over all elements `xₙ` in `s` and `|s|` is the number of elements in `s`.
|
Real.inner_le_Lp_mul_Lq_hasSum_of_nonneg
theorem Real.inner_le_Lp_mul_Lq_hasSum_of_nonneg :
∀ {ι : Type u} {f g : ι → ℝ} {p q : ℝ},
p.IsConjExponent q →
∀ {A B : ℝ},
0 ≤ A →
0 ≤ B →
(∀ (i : ι), 0 ≤ f i) →
(∀ (i : ι), 0 ≤ g i) →
HasSum (fun i => f i ^ p) (A ^ p) →
HasSum (fun i => g i ^ q) (B ^ q) → ∃ C, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i => f i * g i) C
The **Hölder Inequality** is a theorem in mathematical analysis that provides a bound on the scalar product of two non-negative real-valued functions. The theorem states that for any indexed set of real numbers, and for any two functions and two real numbers, if the two real numbers are conjugate exponents, then for any two non-negative real numbers, A and B, if the p-th power of each element in the sequence produced by the first function sums to A^p and the q-th power of each element in the sequence produced by the second function sums to B^q, then there exists a non-negative number C such that the sum of the products of corresponding elements from the two functions is less than or equal to C which is less than or equal to the product of A and B. This is a version for functions producing non-negative real numbers.
More concisely: For non-negative real-valued functions f and g, and for any p, q > 0 with p^(-1) + q^(-1) = 1, the following inequality holds: $\int_X |f(x) \cdot g(x)| dx \leq (\int_X |f(x)|^p dx)^{\frac{1}{p}} (\int_X |g(x)|^q dx)^{\frac{1}{q}}$.
|
ENNReal.inner_le_Lp_mul_Lq
theorem ENNReal.inner_le_Lp_mul_Lq :
∀ {ι : Type u} (s : Finset ι) (f g : ι → ENNReal) {p q : ℝ},
p.IsConjExponent q →
(s.sum fun i => f i * g i) ≤ (s.sum fun i => f i ^ p) ^ (1 / p) * (s.sum fun i => g i ^ q) ^ (1 / q)
The theorem states the Hölder's inequality for functions with values in the extended nonnegative real numbers, in case of finite sums. Specifically, for any type `ι`, any finite set `s` of type `ι`, any two functions `f` and `g` from `ι` to the extended nonnegative real numbers, and any real numbers `p` and `q` that are conjugate exponents (`p` and `q` satisfy the condition `1/p + 1/q = 1`), the sum over `s` of the products `f(i) * g(i)` is less than or equal to the `p`-th power of the sum of `f(i)` raised to the `p`-th power, raised to the power `1/p`, times the `q`-th power of the sum of `g(i)` raised to the `q`-th power, raised to the power `1/q`. This is a generalization of the Cauchy-Schwarz inequality and gives a bound to the scalar product of two functions in terms of their `L^p` and `L^q` norms.
More concisely: For any finite set `s`, functions `f` and `g` from `ι` to the extended nonnegative real numbers, and real numbers `p, q` satisfying `1/p + 1/q = 1`, the following inequality holds: $\sum\_{i \in s} f(i) \cdot g(i) \leq \left(\sum\_{i \in s} f(i)^p\right)^{1/p} \cdot \left(\sum\_{i \in s} g(i)^q\right)^{1/q}$.
|
NNReal.Lp_add_le
theorem NNReal.Lp_add_le :
∀ {ι : Type u} (s : Finset ι) (f g : ι → NNReal) {p : ℝ},
1 ≤ p →
(s.sum fun i => (f i + g i) ^ p) ^ (1 / p) ≤
(s.sum fun i => f i ^ p) ^ (1 / p) + (s.sum fun i => g i ^ p) ^ (1 / p)
The **Minkowski inequality** theorem for `NNReal`-valued functions states that for any index set `ι`, any finite subset `s` of `ι`, any two functions `f` and `g` mapping elements of `ι` to nonnegative real numbers, and any real number `p` greater than or equal to 1, the `L_p` seminorm of the sum of `f` and `g` (calculated as the `p`-th power of the sum of `f(i)` and `g(i)`, summed over `i` in `s`, and then raised to the power of `1/p`) is less than or equal to the sum of the `L_p` seminorms of `f` and `g` separately (calculated similarly but with `f` and `g` separately).
More concisely: For any index set `ι`, finite subset `s`, and nonnegative `NNReal` functions `f` and `g` on `ι`, with real number `p ≥ 1`, the `L_p` seminorm of `f + g` over `s` is less than or equal to the sum of the `L_p` seminorms of `f` and `g` over `s`.
|
NNReal.Lp_add_le_hasSum
theorem NNReal.Lp_add_le_hasSum :
∀ {ι : Type u} {f g : ι → NNReal} {A B : NNReal} {p : ℝ},
1 ≤ p →
HasSum (fun i => f i ^ p) (A ^ p) →
HasSum (fun i => g i ^ p) (B ^ p) → ∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)
The theorem, named "Minkowski inequality", states the property of `NNReal`-valued functions. Given a space of indices `ι` and two functions `f` and `g` defined on this space producing nonnegative real numbers, as well as two nonnegative real numbers `A` and `B`, and a real number `p` that is greater than or equal to 1. If the infinite sum of `p`-th powers of `f` equals `A^p` and the infinite sum of `p`-th powers of `g` equals `B^p`, there exists a nonnegative real number `C` that is less than or equal to `A+B` such that the infinite sum of `p`-th powers of `(f+g)` equals `C^p`. This theorem characterizes a fundamental property of `L_p` seminorms, which is useful in the field of functional analysis and metric spaces.
More concisely: Given two `NNReal`-valued functions `f` and `g` on an index space `ι` with finite `p`-th power sums `A^p` and `B^p` respectively, for `p ≥ 1`, there exists a nonnegative real number `C` such that `(A+B)^p` is less than or equal to the finite `p`-th power sum of `(f+g)`, denoted as `(∥f∥_p + ∥g∥_p)^p`.
|
ENNReal.rpow_sum_le_const_mul_sum_rpow
theorem ENNReal.rpow_sum_le_const_mul_sum_rpow :
∀ {ι : Type u} (s : Finset ι) (f : ι → ENNReal) {p : ℝ},
1 ≤ p → (s.sum fun i => f i) ^ p ≤ ↑s.card ^ (p - 1) * s.sum fun i => f i ^ p
This theorem states that for any positive real number `p` greater than or equal to 1, the `p`-th power of the sum of a function `f i` over a finite set `s`, is always less than or equal to the product of the `p - 1` power of the cardinality of the set `s` and the sum of the `p`-th powers of `f i` over the set `s`. This theorem applies to functions `f` that map from an arbitrary type `ι` to extended nonnegative real numbers, often denoted as `[0, ∞]`. This is a version of the theorem specifically for sums over finite sets with functions valued in extended nonnegative real numbers.
More concisely: For any positive real number `p` and finite set `s`, the `p`-th power of the sum of functions `f i` from type `ι` to `[0, ∞]` is less than or equal to the product of `p-1` times the cardinality of `s` and the sum of the `p`-th powers of the functions `f i` over `s`.
|
Real.Lp_add_le
theorem Real.Lp_add_le :
∀ {ι : Type u} (s : Finset ι) (f g : ι → ℝ) {p : ℝ},
1 ≤ p →
(s.sum fun i => |f i + g i| ^ p) ^ (1 / p) ≤
(s.sum fun i => |f i| ^ p) ^ (1 / p) + (s.sum fun i => |g i| ^ p) ^ (1 / p)
The theorem, called the Minkowski inequality, states that for any finite set `s`, two functions `f` and `g` from elements of the set to real numbers, and a real number `p` greater than or equal to 1, the `L_p` seminorm (or `L_p` norm) of the sum of these two functions is less than or equal to the sum of their individual `L_p` seminorms. In this context, the `L_p` seminorm of a function is defined as the pth root of the sum of the absolute values of the function values to the power of `p`.
More concisely: For any finite set `s`, functions `f` and `g` from `s` to real numbers, and real number `p ≥ 1`, the `L_p` seminorm of `f + g` is less than or equal to the sum of the `L_p` seminorms of `f` and `g`.
|
Real.geom_mean_le_arith_mean_weighted
theorem Real.geom_mean_le_arith_mean_weighted :
∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
(∀ i ∈ s, 0 ≤ w i) →
(s.sum fun i => w i) = 1 → (∀ i ∈ s, 0 ≤ z i) → (s.prod fun i => z i ^ w i) ≤ s.sum fun i => w i * z i
The **AM-GM inequality** theorem states that, for any set `s` of elements of arbitrary type `ι`, along with two functions `w` and `z` mapping `ι` to nonnegative real numbers, if all the weights `w i` are nonnegative and sum up to 1, and all the values `z i` are nonnegative, then the weighted geometric mean of the `z i` (represented by the product of `z i ^ w i` over all `i` in `s`) is less than or equal to their weighted arithmetic mean (represented by the sum of `w i * z i` over all `i` in `s`). In mathematical notation, this is represented as: if $\sum_{i \in s} w_i = 1$ and $0 \leq w_i, z_i$ for all $i \in s$, then $\prod_{i \in s} z_i^{w_i} \leq \sum_{i \in s} w_i * z_i$.
More concisely: For any set `s` with nonnegative weights `wi` summing to 1 and nonnegative values `zi`, the geometric mean of `zi` weighted by `wi` is less than or equal to the arithmetic mean of `wi` multiplied by `zi`. In mathematical notation: $\prod_{i \in s} z_i^{w_i} \leq \sum_{i \in s} w_i * z_i$.
|
NNReal.young_inequality
theorem NNReal.young_inequality :
∀ (a b : NNReal) {p q : NNReal}, p.IsConjExponent q → a * b ≤ a ^ ↑p / p + b ^ ↑q / q
This is the nonnegative real number version of **Young's Inequality**. The theorem states that for any nonnegative real numbers `a` and `b`, and any pair of nonnegative real numbers `p` and `q` that are conjugate exponents (as defined by the `p.IsConjExponent q` condition), the product of `a` and `b` is always less than or equal to the sum of `a` to the power of `p` divided by `p` and `b` to the power of `q` divided by `q`. This version is stated specifically for nonnegative real numbers to avoid having to establish that `p` and `q` are nonnegative for the denominators in the inequality.
More concisely: For nonnegative real numbers `a`, `b`, and conjugate exponents `p`, `q`, the inequality `a * b <= a^p / p + b^q / q` holds.
|
NNReal.young_inequality_real
theorem NNReal.young_inequality_real :
∀ (a b : NNReal) {p q : ℝ}, p.IsConjExponent q → a * b ≤ a ^ p / p.toNNReal + b ^ q / q.toNNReal
This theorem is the non-negative real numbers (`NNReal`) version of Young's inequality with real conjugate exponents. It states that for any two non-negative real numbers `a` and `b`, and any two real numbers `p` and `q` that are conjugate exponents (meaning `1/p + 1/q = 1`), the inequality `a * b ≤ a ^ p / p + b ^ q / q` holds. Here, the operations of exponentiation and division are performed in the field of non-negative real numbers.
More concisely: For any non-negative real numbers `a` and `b` and conjugate exponents `p, q` with `1/p + 1/q = 1`, the inequality `a * b ≤ a ^ p / p + b ^ q / q` holds in the non-negative real numbers.
|
NNReal.rpow_sum_le_const_mul_sum_rpow
theorem NNReal.rpow_sum_le_const_mul_sum_rpow :
∀ {ι : Type u} (s : Finset ι) (f : ι → NNReal) {p : ℝ},
1 ≤ p → (s.sum fun i => f i) ^ p ≤ ↑s.card ^ (p - 1) * s.sum fun i => f i ^ p
The theorem `NNReal.rpow_sum_le_const_mul_sum_rpow` states that for any finite set `s` and any function `f` from `s` to the nonnegative real numbers, and for any real number `p` such that `1 ≤ p`, the `p`-th power of the sum of `f(i)` over all `i` in `s` is less than or equal to the cardinality of `s` raised to the power of `(p - 1)` multiplied by the sum of the `p`-th powers of `f(i)` over all `i` in `s`. This is a version of Hölder's inequality for sums over finite sets, where the functions take values in the nonnegative reals.
More concisely: For any finite set `s` and function `f` mapping `s` to non-negative reals, and for any `1 ≤ p`, the sum of `p`-th powers of `f(i)` over `i` in `s` is less than or equal to the cardinality of `s` raised to the power of `(p - 1)` times the sum of `f(i)` raised to the power of `p` over all `i` in `s`.
|
Real.young_inequality
theorem Real.young_inequality : ∀ (a b : ℝ) {p q : ℝ}, p.IsConjExponent q → a * b ≤ |a| ^ p / p + |b| ^ q / q := by
sorry
This is a statement of **Young's inequality** for arbitrary real numbers. Given any two real numbers `a` and `b`, and two more real numbers `p` and `q` such that `p` is a conjugate exponent of `q` (denoted as `p.IsConjExponent q` in Lean), the product of `a` and `b` is less than or equal to the sum of `a` raised to the power of `p` divided by `p` and `b` raised to the power of `q` divided by `q`. The absolute value function is applied to `a` and `b` when calculating these powers, so the result holds regardless of the signs of `a` and `b`.
More concisely: For any real numbers `a` and `b` and conjugate exponents `p, q` with `p.IsConjExponent q`, we have $|a|^p \cdot |b|^q \leqslant |a|^p + |b|^q$.
|
NNReal.geom_mean_le_arith_mean_weighted
theorem NNReal.geom_mean_le_arith_mean_weighted :
∀ {ι : Type u} (s : Finset ι) (w z : ι → NNReal),
(s.sum fun i => w i) = 1 → (s.prod fun i => z i ^ ↑(w i)) ≤ s.sum fun i => w i * z i
The theorem `NNReal.geom_mean_le_arith_mean_weighted` is a statement of the AM-GM inequality (Arithmetic Mean-Geometric Mean Inequality), specifically for the weighted version of the inequality with nonnegative real valued functions. It states that for any type `ι` and any finite set of elements of this type (`s : Finset ι`), given two functions `w` and `z` that map each element of the finite set to a nonnegative real number, if the sum of the `w(i)` values for all `i` in the finite set equals 1, then the product over all `i` in the set of `z(i)` raised to the power of `w(i)` is less than or equal to the sum over all `i` in the set of `w(i)` multiplied by `z(i)`. This is essentially saying that the geometric mean of the set is less than or equal to the weighted arithmetic mean.
More concisely: For any finite set and functions mapping elements to nonnegative real numbers with sum of weights equal to 1, the geometric mean of these functions is less than or equal to the weighted arithmetic mean.
|
NNReal.inner_le_Lp_mul_Lq_tsum
theorem NNReal.inner_le_Lp_mul_Lq_tsum :
∀ {ι : Type u} {f g : ι → NNReal} {p q : ℝ},
p.IsConjExponent q →
(Summable fun i => f i ^ p) →
(Summable fun i => g i ^ q) →
(Summable fun i => f i * g i) ∧
∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
The Hölder's Inequality theorem states that for any type `ι`, functions `f` and `g` from `ι` to nonnegative real numbers, and real numbers `p` and `q` which are conjugate exponents, if the infinite sums of the `p`-th powers of `f(i)` and the `q`-th powers of `g(i)` exist (are summable), then the infinite sum of the products `f(i) * g(i)` also exists, and is less than or equal to the product of the `p`-th root of the sum of `p`-th powers of `f(i)` and the `q`-th root of the sum of `q`-th powers of `g(i)`. This is a version of Hölder's inequality for nonnegative real-valued functions.
More concisely: For real numbers p, q > 0 with p^{-1} + q^{-1} = 1, and functions f, g from an index set ι to nonnegative real numbers with summable p-th and q-th powers, the sum of products f(i) * g(i) is less than or equal to the product of the p-th root of the sum of the p-th powers of f(i) and the q-th root of the sum of the q-th powers of g(i), for all i in ι.
|
NNReal.Lp_add_le_tsum
theorem NNReal.Lp_add_le_tsum :
∀ {ι : Type u} {f g : ι → NNReal} {p : ℝ},
1 ≤ p →
(Summable fun i => f i ^ p) →
(Summable fun i => g i ^ p) →
(Summable fun i => (f i + g i) ^ p) ∧
(∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤
(∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
The theorem states the **Minkowski inequality** for non-negative real-valued functions. Specifically, given any type `ι`, two functions `f` and `g` from `ι` to non-negative real numbers, and a real number `p` greater than or equal to 1, if the p-th powers of `f` and `g` are both summable, then the p-th power of the sum of `f` and `g` is also summable. Furthermore, the p-th root of the sum of these p-th powers is less than or equal to the sum of the p-th roots of the sum of the p-th powers of `f` and `g` individually. In mathematical terms, assume ∑(f(i)^p) and ∑(g(i)^p) are both convergent, then ∑((f(i) + g(i))^p) is also convergent. Moreover, (∑(f(i) + g(i))^p)^(1/p) ≤ (∑f(i)^p)^(1/p) + (∑g(i)^p)^(1/p). This theorem is a version of the Minkowski inequality for `NNReal`-valued functions, and is useful when the infinite sums are already expressed as p-th powers.
More concisely: Given two non-negative real-valued functions `f` and `g` from an index type `ι` and real number `p ≥ 1`, if the p-th powers of `f` and `g` are summable, then the p-th power of their sum is also summable and their p-th roots of the sum of the p-th powers satisfy the inequality (∑((f(i) + g(i))^p))^(1/p) ≤ (∑(f(i)^p)^(1/p) + ∑(g(i)^p)^(1/p)).
|
Real.inner_le_Lp_mul_Lq_of_nonneg
theorem Real.inner_le_Lp_mul_Lq_of_nonneg :
∀ {ι : Type u} (s : Finset ι) {f g : ι → ℝ} {p q : ℝ},
p.IsConjExponent q →
(∀ i ∈ s, 0 ≤ f i) →
(∀ i ∈ s, 0 ≤ g i) →
(s.sum fun i => f i * g i) ≤ (s.sum fun i => f i ^ p) ^ (1 / p) * (s.sum fun i => g i ^ q) ^ (1 / q)
The **Hölder inequality** is a theorem that states the following: for any finite set 's', and for any two real-valued nonnegative functions 'f' and 'g' defined on that set, if 'p' and 'q' are conjugate exponents, then the sum of the product of 'f' and 'g' over the set 's' is less than or equal to the 'p'-th power of the sum of the 'p'-th power of 'f' raised to the power of 1/p times the 'q'-th power of the sum of the 'q'-th power of 'g' raised to the power of 1/q. This provides a bound on the scalar product of two functions in terms of their `L^p` and `L^q` norms.
More concisely: For any finite set 's' and real-valued nonnegative functions 'f' and 'g' on 's', if 'p' and 'q' are conjugate exponents then $\sum\_{i \in s} f(i)g(i) \leq (\sum\_{i \in s} |f(i)|^p)^{1/p} (\sum\_{i \in s} |g(i)|^q)^{1/q}$ holds.
|
NNReal.inner_le_Lp_mul_Lq_hasSum
theorem NNReal.inner_le_Lp_mul_Lq_hasSum :
∀ {ι : Type u} {f g : ι → NNReal} {A B : NNReal} {p q : ℝ},
p.IsConjExponent q →
HasSum (fun i => f i ^ p) (A ^ p) →
HasSum (fun i => g i ^ q) (B ^ q) → ∃ C ≤ A * B, HasSum (fun i => f i * g i) C
The theorem is a version of the Hölder's Inequality for nonnegative real-valued functions. It states that for any type `ι` and for any two functions `f` and `g` from `ι` to nonnegative real numbers, along with nonnegative real numbers `A` and `B`, and real numbers `p` and `q`; if `p` and `q` are conjugate exponents(i.e., their reciprocals sum up to 1), and if the infinite series of the `p`-th power of `f` sums up to `A^p` and the infinite series of `q`-th power of `g` sums up to `B^q`, then there exists a nonnegative real number `C` less than or equal to the product of `A` and `B`, such that the infinite series of the product of `f` and `g` sums up to `C`. This is essentially stating that the scalar product of two functions is bounded by the product of their `L^p` and `L^q` norms, where `p` and `q` are conjugate exponents.
More concisely: For any type `ι`, given nonnegative real-valued functions `f` and `g` from `ι` to the real numbers, and real numbers `A`, `B`, `p`, and `q` with `p > 0`, `q > 0`, and `p^{-1} + q^{-1} = 1`, if the series of `f^p` and `g^q` sum up to `A^p` and `B^q` respectively, then there exists a nonnegative real number `C` less than or equal to `A * B`, such that the series of `f * g` sums up to `C`.
|
Real.Lp_add_le_hasSum_of_nonneg
theorem Real.Lp_add_le_hasSum_of_nonneg :
∀ {ι : Type u} {f g : ι → ℝ} {p : ℝ},
1 ≤ p →
(∀ (i : ι), 0 ≤ f i) →
(∀ (i : ι), 0 ≤ g i) →
∀ {A B : ℝ},
0 ≤ A →
0 ≤ B →
HasSum (fun i => f i ^ p) (A ^ p) →
HasSum (fun i => g i ^ p) (B ^ p) →
∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => (f i + g i) ^ p) (C ^ p)
The Minkowski Inequality theorem, as provided here, is a version tailored for real-valued functions. For any index type `ι` and any real-valued functions `f` and `g` on `ι`, and a real number `p` greater than or equal to 1, if each element of both `f` and `g` is nonnegative and has a sum `A` and `B` respectively which are nonnegative, and can be expressed as the `p`-th powers of these sums, then there exists a nonnegative real number `C` that is less than or equal to the sum of `A` and `B`, such that the infinite sum of the `p`-th powers of the sums of corresponding elements of `f` and `g` equals to the `p`-th power of `C`. This theorem essentially asserts that in the given conditions, the `L_p` seminorm of the infinite sum of `f` and `g` is less than or equal to the infinite sum of the `L_p` seminorms of `f` and `g`.
More concisely: For any index type `ι` and real-valued functions `f` and `g` on `ι` with nonnegative and summable elements, and real number `p ≥ 1`, if the `p`-th powers of the sums of `f` and `g` are nonnegative and equal to `A` and `B` respectively, then there exists a nonnegative constant `C` such that the `L_p` norm of the sum of `f` and `g` is less than or equal to the sum of the `L_p` norms of `f` and `g`, i.e., $\left(\sum\limits_{i\in ι}|f(i)|^p+\sum\limits_{i\in ι}|g(i)|^p\right)^{\frac{1}{p}}\leq (\sum\limits_{i\in ι}C)^ {\frac{1}{p}}$.
|
Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg
theorem Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg :
∀ {ι : Type u} (s : Finset ι) {f : ι → ℝ} {p : ℝ},
1 ≤ p → (∀ i ∈ s, 0 ≤ f i) → (s.sum fun i => f i) ^ p ≤ ↑s.card ^ (p - 1) * s.sum fun i => f i ^ p
Given a finite set `s` of type `ι` and a function `f` from `ι` to nonnegative real numbers, and a real number `p` such that `1 ≤ p`, this theorem states that the `p`-th power of the sum of `f(i)` for all `i` in `s` is less than or equal to the size of the set `s` raised to the power of `p - 1` times the sum of `f(i)^p` for all `i` in `s`. In mathematical terms, it asserts that if `f : ι → ℝ` is a nonnegative function, then `(∑i in s, f i) ^ p ≤ |s|^(p-1) * ∑i in s, (f i)^p` when `1 ≤ p`.
More concisely: For any finite set `s` and nonnegative function `f` from `s` to the real numbers, and for any `1 ≤ p`, the `p`-th power of the sum of `f(i)` for all `i` in `s` is less than or equal to the size of `s` raised to the power of `p-1` times the sum of `f(i)^p` for all `i` in `s`.
|
Real.inner_le_Lp_mul_Lq
theorem Real.inner_le_Lp_mul_Lq :
∀ {ι : Type u} (s : Finset ι) (f g : ι → ℝ) {p q : ℝ},
p.IsConjExponent q →
(s.sum fun i => f i * g i) ≤ (s.sum fun i => |f i| ^ p) ^ (1 / p) * (s.sum fun i => |g i| ^ q) ^ (1 / q)
The theorem is a version of the Hölder's Inequality, stated for real-valued functions and sums over finite sets. It asserts that the sum of the product of two functions `f` and `g` over a finite set `s` is bounded above by the product of the `L^p` norm of `f` and the `L^q` norm of `g`, where `p` and `q` are real numbers and conjugate exponents. In other words, multiplying the functions and summing over the set won't result in a value greater than the product of the sums of each function raised to its respective exponent and then root-normalized.
More concisely: For real-valued functions `f` and `g` on a finite set `s` and real numbers `p, q > 0` with `1/p + 1/q = 1`, the sum of the products `∑ i in s (f i * g i)` is bounded by `∥f∥ₕ_s * ∥g∥ₗ'_s`, where `∥f∥ₕ_s` and `∥g∥ₗ'_s` denote the `L^p` and `L^q` norms of `f` and `g` on `s`, respectively.
|
NNReal.isGreatest_Lp
theorem NNReal.isGreatest_Lp :
∀ {ι : Type u} (s : Finset ι) (f : ι → NNReal) {p q : ℝ},
p.IsConjExponent q →
IsGreatest ((fun g => s.sum fun i => f i * g i) '' {g | (s.sum fun i => g i ^ q) ≤ 1})
((s.sum fun i => f i ^ p) ^ (1 / p))
The theorem `NNReal.isGreatest_Lp` states that for any finite set `s`, any function `f` from `s` to the nonnegative real numbers, and any pair of real numbers `p` and `q` such that `p` is a conjugate exponent of `q`, the `L_p` seminorm of the vector `f` is the greatest value of the inner product `∑ i in s, f i * g i` over all functions `g` such that the `L_q` seminorm of `g` is less than or equal to one. In other words, the `L_p` seminorm of `f` is the largest possible inner product with a vector that has `L_q` seminorm at most one, where `p` and `q` are conjugate exponents.
More concisely: For any finite set, function to non-negative real numbers, and conjugate exponents p and q, the Lp seminorm of a function is the maximum inner product with a function of Lq seminorm less than or equal to one.
|
NNReal.inner_le_Lp_mul_Lq
theorem NNReal.inner_le_Lp_mul_Lq :
∀ {ι : Type u} (s : Finset ι) (f g : ι → NNReal) {p q : ℝ},
p.IsConjExponent q →
(s.sum fun i => f i * g i) ≤ (s.sum fun i => f i ^ p) ^ (1 / p) * (s.sum fun i => g i ^ q) ^ (1 / q)
The theorem you provided describes Hölder's inequality, which limits the size of the scalar product of two functions, `f` and `g`, defined on a finite set `s`. The scalar product is bounded by the product of two quantities: the `p`-th power of the `L^p` norm of `f` (the sum of the `p`-th powers of the values of `f`, raised to the power `1/p`) and the `q`-th power of the `L^q` norm of `g` (the sum of the `q`-th powers of the values of `g`, raised to the power `1/q`). The conditions for this to hold are that `f` and `g` are nonnegative real-valued functions and that `p` and `q` are real numbers such that they are conjugate exponents, meaning `1/p + 1/q = 1`.
More concisely: For nonnegative real-valued functions `f` and `g` on a finite set `s`, their scalar product is bounded by the product of `(sum (map (lambda x, (f x)^p) s).(pow 1/p) ^-1)` and `(sum (map (lambda x, (g x)^q) s).(pow 1/q) ^-1)`, where `p` and `q` are real numbers satisfying `1/p + 1/q = 1`.
|
Real.young_inequality_of_nonneg
theorem Real.young_inequality_of_nonneg :
∀ {a b p q : ℝ}, 0 ≤ a → 0 ≤ b → p.IsConjExponent q → a * b ≤ a ^ p / p + b ^ q / q
This is a version of **Young's inequality** for nonnegative real numbers. The theorem states that for any real numbers `a`, `b`, `p`, and `q`, where `a` and `b` are nonnegative and `p` and `q` are conjugate exponents (that is, `p` and `q` satisfy the relation `1/p + 1/q = 1`), the product `a * b` is less than or equal to `a` raised to the power `p` divided by `p` plus `b` raised to the power `q` divided by `q`.
More concisely: For nonnegative real numbers `a` and `b` and conjugate exponents `p` and `q` (satisfying `1/p + 1/q = 1`), `a * b ≤ a^p / p + b^q / q`.
|
NNReal.geom_mean_le_arith_mean2_weighted
theorem NNReal.geom_mean_le_arith_mean2_weighted :
∀ (w₁ w₂ p₁ p₂ : NNReal), w₁ + w₂ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ ≤ w₁ * p₁ + w₂ * p₂
The theorem `NNReal.geom_mean_le_arith_mean2_weighted` states the weighted Arithmetic Mean-Geometric Mean (AM-GM) inequality for two nonnegative real numbers. Specifically, for any four nonnegative real numbers `w₁`, `w₂`, `p₁`, and `p₂`, where `w₁` and `w₂` add up to 1, the geometric mean (given by `p₁` raised to the power `w₁` times `p₂` raised to the power `w₂`) is always less than or equal to the arithmetic mean (`w₁` times `p₁` plus `w₂` times `p₂`).
More concisely: For any nonnegative real numbers `p₁`, `p₂` and weights `w₁`, `w₂` (`w₁ + w₂ = 1`), the geometric mean `w₁ * p₁^(Real.log Base 2 w₁) * w₂ * p₂^(Real.log Base 2 w₂)` is less than or equal to the arithmetic mean `(w₁ * p₁ + w₂ * p₂)`.
|
Real.Lp_add_le_of_nonneg
theorem Real.Lp_add_le_of_nonneg :
∀ {ι : Type u} (s : Finset ι) {f g : ι → ℝ} {p : ℝ},
1 ≤ p →
(∀ i ∈ s, 0 ≤ f i) →
(∀ i ∈ s, 0 ≤ g i) →
(s.sum fun i => (f i + g i) ^ p) ^ (1 / p) ≤
(s.sum fun i => f i ^ p) ^ (1 / p) + (s.sum fun i => g i ^ p) ^ (1 / p)
The theorem, titled "Minkowski inequality", establishes that for any set of indices 's', any two real-valued nonnegative functions 'f' and 'g', and any real number 'p' greater than or equal to 1, the `L_p` seminorm of the sum of 'f' and 'g' is always less than or equal to the sum of the `L_p` seminorms of 'f' and 'g' individually. The `L_p` seminorm of a function is computed as the p-th root of the sum of the p-th powers of the function values. This version of the theorem is specifically for `ℝ`-valued nonnegative functions.
More concisely: For any set of indices 's', real-valued nonnegative functions 'f' and 'g' on 's', and real number 'p' ≥ 1, the `∥f + g∥\_p` ≤ `∥f∥\_p + ∥g∥\_p` holds for the `L_p` seminorms.
|
Real.inner_le_Lp_mul_Lq_tsum_of_nonneg
theorem Real.inner_le_Lp_mul_Lq_tsum_of_nonneg :
∀ {ι : Type u} {f g : ι → ℝ} {p q : ℝ},
p.IsConjExponent q →
(∀ (i : ι), 0 ≤ f i) →
(∀ (i : ι), 0 ≤ g i) →
(Summable fun i => f i ^ p) →
(Summable fun i => g i ^ q) →
(Summable fun i => f i * g i) ∧
∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
The Hölder inequality theorem asserts that for any two real-valued functions `f` and `g`, indexed over an arbitrary type `ι`, and any real numbers `p` and `q` that are conjugate exponents, if each value of `f` and `g` is non-negative, and if the `p`-th power of `f` and the `q`-th power of `g` both have finite sums (are `Summable`), then not only does the product of `f` and `g` have a finite sum, but this sum is bounded by the product of the `p`-th root of `f`'s `p`-th power sum and the `q`-th root of `g`'s `q`-th power sum. In mathematical notation, this is saying that if ∑`f(i)^p` and ∑`g(i)^q` both exist, then ∑`f(i)*g(i)` also exists and is less than or equal to (∑`f(i)^p`)^(1/p) * (∑`g(i)^q`)^(1/q).
More concisely: For real-valued functions `f` and `g` indexed over an arbitrary type `ι`, if each value is non-negative, `p` and `q` are conjugate exponents, and both the `p`-th power of `f` and the `q`-th power of `g` have finite sums, then the product of `f` and `g` is Summable and their sum is less than or equal to the product of the `p`-th root of `f`'s `p`-th power sum and the `q`-th root of `g`'s `q`-th power sum.
|