The $L^p$ (extended) norm of a function $f : α → E$ with respect to the measure $μ$.
For $1 ≤ p < ∞$, this is $\|f\|_p = \left(\int |f|^p \, dμ\right)^{1/p}$, and for $p = ∞$
it is the essential supremum $\|f\|_∞ = \operatorname{ess\,sup}|f|$. This is a thin wrapper
around MeasureTheory.eLpNorm.
Instances For
For a continuous function $f : α → E$ on a compact space $α$ equipped with a Borel measure of full support, the essential supremum $\|f\|_{L^\infty(μ)}$ coincides with the usual supremum norm $\|f\|_∞$. This is the continuous-case statement of the essential supremum property: on $[a,b]$ with $f \in C([a,b])$, $\|f\|_{L^\infty([a,b])} = \|f\|_\infty$.
Essential supremum properties: (1) for any measurable function $f : α → E$ we have $|f(x)| ≤ \|f\|_{L^\infty(μ)}$ for almost every $x$, and (2) on a compact Hausdorff space with a Borel measure of full support, the essential supremum of a continuous function $f : C(α, E)$ equals its usual supremum norm.
Integrability part of Hölder's inequality: if $f \in L^p(μ)$ and $g \in L^q(μ)$ with $\frac{1}{p} + \frac{1}{q} = 1$, then the pointwise product $f \cdot g$ is integrable.
Norm part of Hölder's inequality: if $f \in L^p(μ)$ and $g \in L^q(μ)$ with $\frac{1}{p} + \frac{1}{q} = 1$, then $\|fg\|_{L^1(μ)} ≤ \|f\|_{L^p(μ)} \cdot \|g\|_{L^q(μ)}$.
Hölder's inequality for $L^p$ spaces: if $1 ≤ p, q ≤ ∞$ with $\frac{1}{p} + \frac{1}{q} = 1$ and $f, g : α → 𝕜$ are measurable with $f \in L^p(μ)$ and $g \in L^q(μ)$, then $fg$ is integrable and $\int_E |fg| \, dμ ≤ \|f\|_{L^p(μ)} \cdot \|g\|_{L^q(μ)}$.
Minkowski's inequality for $L^p$ spaces: for $1 ≤ p ≤ ∞$ and measurable functions $f, g : α → E$, $\|f + g\|_{L^p(μ)} ≤ \|f\|_{L^p(μ)} + \|g\|_{L^p(μ)}$. This is the triangle inequality for the $L^p$ norm.
Riesz-Fischer theorem: for $1 ≤ p ≤ ∞$ and a complete normed space $E$, the space $L^p(μ; E)$ is complete, hence a Banach space.
The $L^p$ space $L^p(μ; E) = \{f : α → E : f \text{ measurable and } \|f\|_p < ∞\}$,
quotiented by the equivalence relation of almost-everywhere equality. Implemented as a thin
wrapper around MeasureTheory.Lp.
Instances For
For a measurable set $S \subset ℝ$ and a measurable function $g : ℝ → [0, ∞]$, the integral $\int_S g$ equals the supremum over $n ∈ ℕ$ of the truncated integrals $\int_{[-n,n] \cap S} g$. This is a monotone convergence statement used to characterize $L^p$ membership via restricted integrals.
Characterization of $L^p$ membership in terms of restricted integrals: for $E \subset ℝ$ measurable and $1 ≤ p < ∞$, a measurable function $f$ belongs to $L^p(E)$ if and only if $\lim_{n \to \infty} \int_{[-n, n] \cap E} |f|^p < ∞$.
$L^p(μ; E)$ is a normed additive commutative group for $1 ≤ p ≤ ∞$, with norm $\|\cdot\|_p$. This is part of the statement that $L^p(E)$ is a normed vector space.
$L^p(μ; E)$ is a normed vector space over $𝕜$ for $1 ≤ p ≤ ∞$. Together with the additive group instance, this gives the statement that $L^p(E)$ is a normed vector space under $\|\cdot\|_p$.
Continuous functions vanishing at the endpoints are dense in $L^p([a, b])$: for $a < b$, $1 ≤ p < ∞$, $f \in L^p([a, b])$ and $\varepsilon > 0$, there exists $g \in C([a, b])$ with $g(a) = g(b) = 0$ such that $\|f - g\|_p < \varepsilon$.
Functions with polynomial decay are in $L^p(ℝ)$ for all $p ≥ 1$: if $f : ℝ → E$ is measurable and there exist constants $C ≥ 0$ and $q > 1$ such that $\|f(x)\| ≤ C(1 + |x|)^{-q}$ for almost every $x \in ℝ$, then $f \in L^p(ℝ)$ for every $1 ≤ p ≤ ∞$.