English
For a function f: α → ε, a real q, and a measure μ, eLpNorm'(f,q,μ) is defined as the q-th power of the (extended) integral of the q-th power of the norm of f, raised to the 1/q.
Русский
Для функции f: α → ε, действительного q и меры μ величина eLpNorm'(f,q,μ) определяется как (∫ ‖f‖^q dμ)^{1/q}.
LaTeX
$$$\\mathrm{eLpNorm}'(f,q,\\mu) = \\left(\\int^{\\! -\\!} a \\; \\|f(a)\\|_{\\varepsilon}^{\\,q} \\\\partial\\mu(a)\\right)^{1/q}$$$
Lean4
/-- `(∫ ‖f a‖^q ∂μ) ^ (1/q)`, which is a seminorm on the space of measurable functions for which
this quantity is finite.
Note: this is a purely auxiliary quantity; lemmas about `eLpNorm'` should only be used to
prove results about `eLpNorm`; every `eLpNorm'` lemma should have a `eLpNorm` version. -/
def eLpNorm' {_ : MeasurableSpace α} (f : α → ε) (q : ℝ) (μ : Measure α) : ℝ≥0∞ :=
(∫⁻ a, ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)
