ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top
theorem ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : ℝ},
p.IsConjExponent q →
∀ {f g : α → ENNReal},
AEMeasurable f μ →
∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤ →
∫⁻ (a : α), g a ^ q ∂μ ≠ ⊤ →
∫⁻ (a : α), f a ^ p ∂μ ≠ 0 →
∫⁻ (a : α), g a ^ q ∂μ ≠ 0 →
∫⁻ (a : α), (f * g) a ∂μ ≤
(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
The theorem `ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top` represents Hölder's inequality for the case of finite non-zero integrals. Given a measure space `α` with a measurable space structure, a measure `μ`, exponents `p` and `q` such that `p` is the conjugate exponent of `q`, and almost everywhere measurable functions `f` and `g` mapping from `α` to the extended nonnegative real numbers. If the p-integral of `f` and the q-integral of `g` are both finite and non-zero, then the integral of the product of `f` and `g` is less than or equal to the pth root of the p-integral of `f` times the qth root of the q-integral of `g`.
More concisely: If `μ` is a measure on a measurable space `α`, `p` and `q` are conjugate exponents, `f` and `g` are almost everywhere measurable functions mapping from `α` to the extended nonnegative real numbers with finite and non-zero `p`-th and `q`-th integrals respectively, then `∫(f * g) dμ ≤ (∫|f|^p dμ)^(1/p) * (∫|g|^q dμ)^(1/q)`.
|
ENNReal.lintegral_mul_prod_norm_pow_le
theorem ENNReal.lintegral_mul_prod_norm_pow_le :
∀ {α : Type u_2} {ι : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Finset ι)
{g : α → ENNReal} {f : ι → α → ENNReal},
AEMeasurable g μ →
(∀ i ∈ s, AEMeasurable (f i) μ) →
∀ (q : ℝ) {p : ι → ℝ},
(q + s.sum fun i => p i) = 1 →
0 ≤ q →
(∀ i ∈ s, 0 ≤ p i) →
∫⁻ (a : α), g a ^ q * s.prod fun i => f i a ^ p i ∂μ ≤
(∫⁻ (a : α), g a ∂μ) ^ q * s.prod fun i => (∫⁻ (a : α), f i a ∂μ) ^ p i
This theorem is a generalization of Hölder's inequality for functions defined on a measurable space. Given a finite set `s` of indices, a measurable function `g` and a family of measurable functions `f` indexed by elements of `s`, all defined on a measure space `α` with measure `μ`, and real numbers `q` and `p` (also indexed by elements of `s`) satisfying certain conditions, the theorem states that the integral of `g` raised to the power `q` times the product of each `f(i)` raised to the power `p(i)`, is less than or equal to the integral of `g` raised to the power `q` times the product of the integral of each `f(i)` raised to the power `p(i)`. The conditions on `q` and `p` are that `q + sum(p(i) for i in s) = 1`, `q` is nonnegative, and each `p(i)` is nonnegative.
More concisely: Given measurable functions `g` and a family `f(i)` on a measure space `(α, μ)`, and real numbers `q` and `p(i)` satisfying `q + ∑(p(i): i ∈ I) = 1`, `q, p(i) ≥ 0` for all `i`, Hölder's inequality states that `∫(g⁴(x) ∏(f⁴(i)(x))ₙ di) ≤ ∫(g⁴(x) ∏(∫(f⁴(i)(x) di) p(i)) dp)`.
|
ENNReal.lintegral_Lp_add_le_of_le_one
theorem ENNReal.lintegral_Lp_add_le_of_le_one :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {f g : α → ENNReal},
AEMeasurable f μ →
0 ≤ p →
p ≤ 1 →
(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
2 ^ (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
This theorem is a variant of Minkowski's inequality applied to functions mapping from an arbitrary type `α` to the extended nonnegative real numbers (usually denoted as [0, ∞]). Given a measure space defined over `α`, a measure `μ`, and two functions `f` and `g` that are almost everywhere measurable with respect to `μ`, if a real number `p` is nonnegative and also less than or equal to 1, then the `ℒp` seminorm (given by the `p`-th root of the integral of the function raised to the power `p`) of the sum of `f` and `g` is bounded above by a constant multiple of the sum of their `ℒp` seminorms. The constant multiple is given by 2 raised to the power of (1 / `p` - 1). This inequality provides a control over the sum of the functions in terms of their individual `ℒp` seminorms when `p` is less than or equal to 1.
More concisely: For any measure space `(α, μ)`, almost everywhere measurable functions `f` and `g` from `α` to the extended nonnegative real numbers, and `p` in the open unit interval (0, 1], the `ℒp` seminorm of `f + g` is bounded above by 2^(1/p) times the sum of their individual `ℒp` seminorms.
|
ENNReal.lintegral_mul_le_Lp_mul_Lq
theorem ENNReal.lintegral_mul_le_Lp_mul_Lq :
∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {p q : ℝ},
p.IsConjExponent q →
∀ {f g : α → ENNReal},
AEMeasurable f μ →
AEMeasurable g μ →
∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
Hölder's inequality for functions `α → ℝ≥0∞` states that: given a measure space `α` with a measure `μ`, and two real numbers `p` and `q` that are conjugate exponents, for any two almost everywhere measurable functions `f` and `g` from `α` to the extended nonnegative real numbers, the integral of the product of these two functions with respect to `μ` is bounded by the product of their `ℒp` and `ℒq` seminorms raised to the power of `1/p` and `1/q` respectively. This means that the amount by which the product of `f` and `g` integrates over the whole space is at most the product of the `p`-th power integral of `f` and the `q`-th power integral of `g`, each taken to the reciprocal of their respective powers.
More concisely: For measurable functions $f, g : \alpha \to \mathbb{R} \cup \{+\infty\}$, and a measure $\mu$ on $\alpha$, if $p, q > 0$ satisfy $\frac{1}{p} + \frac{1}{q} = 1$, then $\int_\alpha |f(x) g(x)| d\mu \leq \left(\int_\alpha |f(x)|^p d\mu\right)^\frac{1}{p} \left(\int_\alpha |g(x)|^q d\mu\right)^\frac{1}{q}$.
|
NNReal.lintegral_mul_le_Lp_mul_Lq
theorem NNReal.lintegral_mul_le_Lp_mul_Lq :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : ℝ},
p.IsConjExponent q →
∀ {f g : α → NNReal},
AEMeasurable f μ →
AEMeasurable g μ →
∫⁻ (a : α), ↑((f * g) a) ∂μ ≤
(∫⁻ (a : α), ↑(f a) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑(g a) ^ q ∂μ) ^ (1 / q)
This is Hölder's inequality for functions mapping to nonnegative real numbers (`α → ℝ≥0`). The theorem states that, for any given measure space `α` and a measure `μ` on that space, if `p` and `q` are conjugate exponents (`p.IsConjExponent q`), and for any two functions `f` and `g` that are almost everywhere measurable (`AEMeasurable f μ` and `AEMeasurable g μ`) mapping from `α` to nonnegative real numbers, the integral of the product of these two functions is bounded by the product of their `ℒp` and `ℒq` seminorms. This is represented mathematically as `∫⁻ (a : α), ↑((f * g) a) ∂μ ≤ (∫⁻ (a : α), ↑(f a) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑(g a) ^ q ∂μ) ^ (1 / q)`.
More concisely: For any measure space and measure, if two almost everywhere measurable functions mapping to nonnegative real numbers have conjugate exponents, then the integral of their product is bounded by the product of their `ℒp` and `ℒq` seminorms.
|
ENNReal.lintegral_prod_norm_pow_le
theorem ENNReal.lintegral_prod_norm_pow_le :
∀ {α : Type u_2} {ι : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Finset ι)
{f : ι → α → ENNReal},
(∀ i ∈ s, AEMeasurable (f i) μ) →
∀ {p : ι → ℝ},
(s.sum fun i => p i) = 1 →
(∀ i ∈ s, 0 ≤ p i) →
∫⁻ (a : α), s.prod fun i => f i a ^ p i ∂μ ≤ s.prod fun i => (∫⁻ (a : α), f i a ∂μ) ^ p i
This theorem is a variation of Hölder's inequality applied to multiple arguments. It says that for all measurable spaces `α` and index types `ι`, and for all measures `μ` on `α`, for any finite set `s` of indices and any function `f` from indices to extended nonnegative real-valued functions on `α`, if every function `f i` is almost everywhere measurable with respect to `μ` for all `i` in `s`, then for any real-valued function `p` on the indices, if the sum of `p i` over all `i` in `s` equals 1, and `p i` is nonnegative for all `i` in `s`, then the integral over `α` of the product over `s` of `f i a` raised to the power `p i` with respect to the measure `μ` is less than or equal to the product over `s` of the integral over `α` of `f i a` with respect to `μ` raised to the power `p i`. In mathematical notation, this is expressed as:
∫ (product over `s` of `f_i(a)^p_i`) dμ ≤ (product over `s` of ∫ `f_i(a)` dμ `^p_i`).
More concisely: For measurable spaces `α`, index types `ι`, measures `μ` on `α`, finite sets `s` of indices, and functions `f` from indices to extended nonnegative real-valued functions on `α`, if every `f i` is almost everywhere measurable with respect to `μ` and `p i` is a nonnegative real number summing to 1, then the integral of the product of `f i a` raised to the power `p i` with respect to `μ` is less than or equal to the product of the integral of `f i a` raised to the power `p i` with respect to `μ`. That is, ∫ (∏ `f_i(a)^p_i`) dμ ≤ ∏ `(∫ f_i(a) dμ ^p_i)`.
|
ENNReal.lintegral_mul_norm_pow_le
theorem ENNReal.lintegral_mul_norm_pow_le :
∀ {α : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
AEMeasurable f μ →
AEMeasurable g μ →
∀ {p q : ℝ},
0 ≤ p →
0 ≤ q →
p + q = 1 → ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
This is a variant of Hölder's inequality applied to two functions `f` and `g`, which are almost everywhere measurable with respect to a given measure `μ`. The theorem states that for any non-negative real numbers `p` and `q` that sum to 1, the integral of the product of `f^p` and `g^q` with respect to `μ` is less than or equal to the product of the `p`-th power of the integral of `f` with respect to `μ` and the `q`-th power of the integral of `g` with respect to `μ`. In mathematical notation, it states that if 0 ≤ p, q and p + q = 1, then ∫ (f^p * g^q) dμ ≤ (∫ f dμ)^p * (∫ g dμ)^q.
More concisely: For measurable functions $f$ and $g$ with respect to a measure $\mu$, and for any $0 \leq p, q$ such that $p + q = 1$, the integral $\int (f^p \cdot g^q) d\mu$ is less than or equal to $(\int f d\mu)^p \cdot (\int g d\mu)^q$.
|
ENNReal.lintegral_Lp_add_le
theorem ENNReal.lintegral_Lp_add_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {f g : α → ENNReal},
AEMeasurable f μ →
AEMeasurable g μ →
1 ≤ p →
(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
**Minkowski's inequality for functions theorem**: Given a measurable space `α`, a measure `μ` on this space, a real number `p` greater than or equal to 1, and two functions `f` and `g` from `α` to the extended nonnegative real numbers (`ENNReal`), both of which are almost everywhere measurable, the `ℒp` seminorm (which is the integral of each function to the power `p`, taken to the power `1/p`) of the sum of these functions is less than or equal to the sum of their respective `ℒp` seminorms. In mathematical notation, this can be written as:
```
(∫ (f + g)^p dμ)^(1/p) ≤ (∫ f^p dμ)^(1/p) + (∫ g^p dμ)^(1/p)
```
More concisely: The `ℒp` seminorm of the sum of two almost everywhere measurable functions on a measurable space with respect to a measure is less than or equal to the sum of their individual `ℒp` seminorms for `p ≥ 1`.
|