MeasureTheory.snorm_smul_le_mul_snorm
theorem MeasureTheory.snorm_smul_le_mul_snorm :
∀ {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : MulActionWithZero 𝕜 E] [inst_3 : BoundedSMul 𝕜 E]
{p q r : ENNReal} {f : α → E},
MeasureTheory.AEStronglyMeasurable f μ →
∀ {φ : α → 𝕜},
MeasureTheory.AEStronglyMeasurable φ μ →
1 / p = 1 / q + 1 / r →
MeasureTheory.snorm (φ • f) p μ ≤ MeasureTheory.snorm φ q μ * MeasureTheory.snorm f r μ
This theorem is a formalization of Hölder's inequality in the context of Lebesgue spaces (`ℒp` spaces). It states that for any measure space `α`, any measure `μ` on `α`, any scalar field `𝕜`, any normed additively commutative group `E`, any `𝕜`-scalar multiplication on `E`, and any exponents `p`, `q`, and `r` in the extended nonnegative real numbers, if `f` is a function from `α` to `E` that is almost everywhere strongly measurable with respect to `μ`, and `φ` is a function from `α` to `𝕜` that is also almost everywhere strongly measurable with respect to `μ`, and if `1/p = 1/q + 1/r`, then the `ℒp` seminorm of the scalar product `φ • f` is less than or equal to the product of `ℒq` seminorm of `φ` and the `ℒr` seminorm of `f`. Note that the `ℒp` seminorm is defined as `0` for `p=0`, as `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞`, and as the essential supremum of `‖f‖` with respect to measure `μ` for `p = ∞`.
More concisely: For any measure space, measure, scalar field, normed additively commutative group, scalar multiplication, and measurable functions `f: α → E` and `φ: α → ℝ`, if `1/p = 1/q + 1/r`, `p, q, r > 0`, and `μ` is a measure on `α`, then the scalar product `φ • f` belongs to the `ℒp` space and satisfies `∥φ • f∥\_p ≤ ∥φ∥\_q * ∥f∥\_r`.
|
MeasureTheory.snorm_le_snorm_mul_snorm'_of_norm
theorem MeasureTheory.snorm_le_snorm_mul_snorm'_of_norm :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} [inst : NormedAddCommGroup E]
[inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.Measure α} {f : α → E}
{g : α → F} {p q r : ENNReal},
MeasureTheory.AEStronglyMeasurable f μ →
MeasureTheory.AEStronglyMeasurable g μ →
∀ (b : E → F → G),
(∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ ≤ ‖f x‖ * ‖g x‖) →
1 / p = 1 / q + 1 / r →
MeasureTheory.snorm (fun x => b (f x) (g x)) p μ ≤
MeasureTheory.snorm f q μ * MeasureTheory.snorm g r μ
This theorem states Hölder's inequality in the context of `ℒp` seminorms on a measure space. Given three extended nonnegative real numbers `p`, `q`, and `r` such that `1/p = 1/q + 1/r`, a measure `μ` on a measurable space, and two functions `f` and `g` from the space to normed additively commutative groups `E` and `F`, which are almost everywhere strongly measurable with respect to `μ`, and a third function `b` from `E` and `F` to a normed additively commutative group `G` such that almost everywhere, the norm of `b (f x) (g x)` is less than or equal to the product of the norms of `f x` and `g x`, the theorem asserts that the `ℒp` seminorm of the function `fun x => b (f x) (g x)` with respect to `μ`, is less than or equal to the product of the `ℒq` seminorm of `f` with respect to `μ` and the `ℒr` seminorm of `g` with respect to `μ`.
More concisely: For measurable functions $f : X \to E$ and $g : X \to F$, and a real number $p > 0$ with conjugate exponents $q, r$ satisfying $1/p = 1/q + 1/r$, the $\ell^p$ norm of the function $x \mapsto b(f(x), g(x))$ is less than or equal to the product of the $\ell^q$ norm of $f$ and the $\ell^r$ norm of $g$ with respect to a measure $\mu$ on a measure space $(X, \Sigma, \mu)$, where $b : E \times F \to G$ is a function for which the norm of $b(f(x), g(x))$ is almost everywhere less than or equal to the product of the norms of $f(x)$ and $g(x)$.
|
MeasureTheory.Memℒp.memℒp_of_exponent_le
theorem MeasureTheory.Memℒp.memℒp_of_exponent_le :
∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
{p q : ENNReal} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : α → E},
MeasureTheory.Memℒp f q μ → p ≤ q → MeasureTheory.Memℒp f p μ
The theorem `MeasureTheory.Memℒp.memℒp_of_exponent_le` states that for any types `α` and `E`, where `α` is equipped with a measurable space structure `m`, `E` is a normed add commutative group, and `μ` is a finite measure on `α`, if a function `f` from `α` to `E` is in the measure space `ℒ^q` (meaning it is almost everywhere strongly measurable and its `q`-norm is finite), then `f` is also in the measure space `ℒ^p` whenever `p` is less than or equal to `q`.
More concisely: If `f` is a function from a measurable space `(α, m)` to a normed add commutative group `E`, equipped with a finite measure `μ`, and `f` belongs to the `L^q` space, then `f` also belongs to the `L^p` space for any `p ≤ q`.
|
MeasureTheory.snorm_le_snorm_mul_snorm_of_nnnorm
theorem MeasureTheory.snorm_le_snorm_mul_snorm_of_nnnorm :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} [inst : NormedAddCommGroup E]
[inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.Measure α} {f : α → E}
{g : α → F} {p q r : ENNReal},
MeasureTheory.AEStronglyMeasurable f μ →
MeasureTheory.AEStronglyMeasurable g μ →
∀ (b : E → F → G),
(∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊) →
1 / p = 1 / q + 1 / r →
MeasureTheory.snorm (fun x => b (f x) (g x)) p μ ≤
MeasureTheory.snorm f q μ * MeasureTheory.snorm g r μ
This theorem is a version of Hölder's inequality. In the context of measure theory, it states that for any measure space `α`, with real-valued, almost everywhere strongly measurable functions `f` and `g`, and a function `b` that maps from the values of `f` and `g` to another real-valued measurable space `G`, such that almost everywhere `b(f(x), g(x))` is less than or equal to the product of the norms of `f(x)` and `g(x)`. If `p`, `q`, and `r` are extended nonnegative real numbers (which includes positive infinity) such that the reciprocals of `p`, `q`, and `r` sum to 1, then the `ℒp` seminorm of the function `b(f, g)` under measure `μ` is less than or equal to the product of the `ℒq` seminorm of `f` and the `ℒr` seminorm of `g`. The `ℒp` seminorm is a measure of the size of a function in `Lp` space, generalizing the concept of norm and absolute value.
More concisely: For measurable functions $f$ and $g$ on a measure space $\alpha$, and a measurable function $b$ satisfying $b(f(x), g(x)) \leq ||f(x)||_p ||g(x)||_q$ almost everywhere, where $\frac{1}{p} + \frac{1}{q} = 1$ and $||.||_p$ is the $L^p$ norm, we have $||b(f, g)||_{L^r} \leq ||f||_{L^p} ||g||_{L^q}$.
|