NNReal.arith_mean_le_rpow_mean
theorem NNReal.arith_mean_le_rpow_mean :
∀ {ι : Type u} (s : Finset ι) (w z : ι → NNReal),
(s.sum fun i => w i) = 1 →
∀ {p : ℝ}, 1 ≤ p → (s.sum fun i => w i * z i) ≤ (s.sum fun i => w i * z i ^ p) ^ (1 / p)
This theorem, named "NNReal.arith_mean_le_rpow_mean", states the following: Given a finite set `s` of some type `ι`, and two functions `w` and `z` that map from `ι` to nonnegative real numbers (`NNReal`), if the sum of the weights `w i` over the set `s` equals 1, then for any real number `p` greater than or equal to 1, the weighted arithmetic mean of `z` (that is, the sum over `s` of `w i * z i`) is less than or equal to the pth power mean of `z` (that is, the pth root of the sum over `s` of `w i * z i ^ p`). This is a form of the generalized mean inequality, specifically for sums over finite sets and for `ℝ≥0`-valued functions with real exponents.
More concisely: Given a finite set and two functions mapping to nonnegative reals with summed weights equal to 1, the weighted arithmetic mean of the functions is less than or equal to the p-th power mean for any p >= 1.
|
NNReal.rpow_arith_mean_le_arith_mean2_rpow
theorem NNReal.rpow_arith_mean_le_arith_mean2_rpow :
∀ (w₁ w₂ z₁ z₂ : NNReal), w₁ + w₂ = 1 → ∀ {p : ℝ}, 1 ≤ p → (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p := by
sorry
The theorem `NNReal.rpow_arith_mean_le_arith_mean2_rpow` states the weighted generalized mean inequality for two nonnegative real numbers and real exponents. More specifically, for any nonnegative real numbers `w₁`, `w₂`, `z₁`, and `z₂`, where `w₁ + w₂` equals 1, and for any real number `p` that is greater than or equal to 1, the p-th power of the sum of `w₁ * z₁` and `w₂ * z₂` is less than or equal to the sum of `w₁ * z₁ ^ p` and `w₂ * z₂ ^ p`. This captures a generalized version of the inequality between the arithmetic mean and the geometric mean.
More concisely: For any nonnegative real numbers $w\_1, w\_2, z\_1,$ and $z\_2$ with $w\_1 + w\_2 = 1,$ and for any real number $p \ge 1,$ we have $w\_1 * z\_1^p + w\_2 * z\_2^p \le (w\_1 * z\_1 + w\_2 * z\_2) ^ p.$
|
NNReal.pow_arith_mean_le_arith_mean_pow
theorem NNReal.pow_arith_mean_le_arith_mean_pow :
∀ {ι : Type u} (s : Finset ι) (w z : ι → NNReal),
(s.sum fun i => w i) = 1 → ∀ (n : ℕ), (s.sum fun i => w i * z i) ^ n ≤ s.sum fun i => w i * z i ^ n
This theorem is a version of the Weighted Generalized Mean Inequality. It states that for any set `s` of type `ι`, any two functions `w` and `z` from `ι` to nonnegative real numbers (`NNReal`), and any natural number `n`, if the sum of the function `w` over the set `s` is equal to 1, then the `n`-th power of the sum of the product of `w i` and `z i` over the set `s` is less than or equal to the sum of the product of `w i` and `z i` raised to the `n`-th power over the set `s`.
In mathematical terms, if $\sum_{i \in s} w(i) = 1$, then $\left( \sum_{i \in s} w(i) \cdot z(i) \right)^n \leq \sum_{i \in s} w(i) \cdot z(i)^n$ for any natural number `n`.
More concisely: For any set `s`, functions `w` and `z` from `s` to nonnegative real numbers with sum `1`, and natural number `n`, the `n`-th power of the weighted sum of `w(i) * z(i)` is less than or equal to the weighted sum of `w(i) * z(i)` raised to the `n`-th power.
|
ENNReal.rpow_arith_mean_le_arith_mean_rpow
theorem ENNReal.rpow_arith_mean_le_arith_mean_rpow :
∀ {ι : Type u} (s : Finset ι) (w z : ι → ENNReal),
(s.sum fun i => w i) = 1 → ∀ {p : ℝ}, 1 ≤ p → (s.sum fun i => w i * z i) ^ p ≤ s.sum fun i => w i * z i ^ p
The theorem `ENNReal.rpow_arith_mean_le_arith_mean_rpow` states the weighted generalized mean inequality for sums over finite sets, with nonnegative extended real-valued functions and real exponents. Specifically, for any type `ι`, given a finite set `s` of `ι`, and two functions `w` and `z` from `ι` to the extended nonnegative real numbers (`ENNReal`), if the sum of `w i` over all `i` in `s` equals 1, then for any real number `p` that is greater than or equal to 1, the `p`-th power of the sum over `s` of the product of `w i` and `z i` is less than or equal to the sum over `s` of the product of `w i` and the `p`-th power of `z i`. This theorem is a variant of the generalized mean inequality in the context of measure theory.
More concisely: For any finite set and functions from the set to the extended nonnegative real numbers with sum of weights equal to 1, the weighted p-th power mean of products is less than or equal to the p-th power mean of weights multiplied by the values. (p >= 1)
|
ENNReal.rpow_arith_mean_le_arith_mean2_rpow
theorem ENNReal.rpow_arith_mean_le_arith_mean2_rpow :
∀ (w₁ w₂ z₁ z₂ : ENNReal), w₁ + w₂ = 1 → ∀ {p : ℝ}, 1 ≤ p → (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
This theorem states the weighted generalized mean inequality for two nonnegative extended real numbers `z₁` and `z₂` and their weights `w₁` and `w₂` respectively, where the sum of weights is 1. For any real exponent `p` that is greater than or equal to 1, the power `p` of the weighted sum of `z₁` and `z₂` is less than or equal to the sum of the individual terms each weighted and raised to the power `p`. In mathematical terms, it denotes that for `w₁, w₂, z₁, z₂ ∈ [0, ∞]`, `w₁ + w₂ = 1`, and for any `p ∈ ℝ` where `1 ≤ p`, `(w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p`.
More concisely: For any nonnegative extended real numbers `z₁`, `z₂`, weights `w₁`, `w₂` with `w₁ + w₂ = 1`, and real exponent `p ≥ 1`, the weighted power `(w₁ * z₁ ^ p + w₂ * z₂ ^ p)` is less than or equal to the power of the weighted sum `(w₁ * z₁ + w₂ * z₂) ^ p`.
|
ENNReal.rpow_add_le_mul_rpow_add_rpow
theorem ENNReal.rpow_add_le_mul_rpow_add_rpow :
∀ (z₁ z₂ : ENNReal) {p : ℝ}, 1 ≤ p → (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
The theorem `ENNReal.rpow_add_le_mul_rpow_add_rpow` states that for any two extended nonnegative real numbers `z₁` and `z₂`, and any real number `p` which is greater or equal to 1, the `p`-th power of the sum of `z₁` and `z₂` is less or equal to 2 raised to the power of `p - 1`, multiplied by the sum of `z₁` and `z₂` each raised to the power of `p`. This is a version of the unweighted mean inequality for two elements of the extended nonnegative real numbers and real exponents.
More concisely: For any extended nonnegative real numbers `z₁` and `z₂` and real number `p ≥ 1`, we have `z₁ ^ p + z₂ ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)`.
|
Real.pow_sum_div_card_le_sum_pow
theorem Real.pow_sum_div_card_le_sum_pow :
∀ {ι : Type u} (s : Finset ι) {f : ι → ℝ} (n : ℕ),
(∀ a ∈ s, 0 ≤ f a) → (s.sum fun x => f x) ^ (n + 1) / ↑s.card ^ n ≤ s.sum fun x => f x ^ (n + 1)
This theorem is a specific case of Jensen's Inequality for sums of powers. It states that, for any finite set `s` of type `ι` and any real-valued function `f` defined on `ι` that is non-negative on `s`, and for any natural number `n`, the sum over `s` of `f`, raised to the power of `(n + 1)`, and divided by the cardinality of `s` raised to the power of `n`, is less than or equal to the sum over `s` of `f` raised to the power of `(n + 1)`.
More concisely: For any finite set `s` with non-negative real-valued function `f` defined on `s`, and integer `n ≥ 0`, the average `(∑ x in s : f x)^(n + 1) / (card s)^n` is less than or equal to the sum `∑ x in s : (f x)^(n + 1)` of `n+1`-th powers of `f` over `s`.
|
NNReal.rpow_add_le_mul_rpow_add_rpow
theorem NNReal.rpow_add_le_mul_rpow_add_rpow :
∀ (z₁ z₂ : NNReal) {p : ℝ}, 1 ≤ p → (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
This theorem, referred to as the unweighted mean inequality, states that for any two nonnegative real numbers `z₁` and `z₂`, and for any real number `p` greater than or equal to 1, the `p`th power of the sum of `z₁` and `z₂` is less than or equal to 2 raised to the power of `p - 1` times the sum of the `p`th powers of `z₁` and `z₂`. In mathematical terms, this can be expressed as: for all `z₁`, `z₂` in ℝ≥0 and for all `p` in ℝ such that `p` ≥ 1, we have `(z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)`.
More concisely: For any nonnegative real numbers `z₁` and `z₂` and real number `p` ≥ 1, the `p`th power of their sum is less than or equal to 2 raised to the power of `p - 1` times the sum of their `p`th powers: `(z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)`.
|
NNReal.rpow_arith_mean_le_arith_mean_rpow
theorem NNReal.rpow_arith_mean_le_arith_mean_rpow :
∀ {ι : Type u} (s : Finset ι) (w z : ι → NNReal),
(s.sum fun i => w i) = 1 → ∀ {p : ℝ}, 1 ≤ p → (s.sum fun i => w i * z i) ^ p ≤ s.sum fun i => w i * z i ^ p
This theorem, referred to as the "Weighted generalized mean inequality", is a version for sums over finite sets, where both the weights (`w`) and the values (`z`) are non-negative real numbers, and the exponents are real numbers. It states that, for any type `ι` and any finite set `s` of `ι`, given a weight function `w` and a value function `z` from `ι` to non-negative real numbers, if the sum of weights is `1`, then for any real number `p` such that `p` is greater than or equal to `1`, the p-th power of the sum of the product of weights and values is less than or equal to the sum of the products of the weights and the p-th power of values. In mathematical notation, this means $\left(\sum_{i\in s} w(i)z(i)\right)^p \leq \sum_{i\in s} w(i)z(i)^p$ when $\sum_{i\in s} w(i) = 1$ and $p\geq1$.
More concisely: Given a finite set `s` with non-negative weights `w` and values `z` such that the sum of weights is `1`, the p-th power of the weighted sum of values is less than or equal to the weighted sum of the p-th power of values for any real number `p >= 1`. In mathematical notation: $\left(\sum\_{i \in s} w(i)z(i)\right)^p \leq \sum\_{i \in s} w(i)z(i)^p$.
|