English
Let s be a finite index set and (f i)_{i∈s} be measurable functions from α to a normed ring. If each f i lies in the corresponding L^{p_i}(μ) for i ∈ s, then the pointwise product ∏_{i∈s} f_i lies in the Lorentz-Lp space L^{(∑_{i∈s} p_i^{-1})^{-1}}(μ).
Русский
Пусть s — конечное множество индексов и (f_i)_{i∈s} — измеримые функции из α в нормированное кольцо. Если для каждого i∈s выполняется f_i ∈ L^{p_i}(μ), то произведение ∏_{i∈s} f_i принадлежит пространству L^{(∑_{i∈s} p_i^{-1})^{-1}}(μ).
LaTeX
$$$\\operatorname{MemLp}\\left(\\omega \\mapsto \\prod_{i \\in s} f_i(\\omega)\\right)\\,\\left(\\sum_{i \\in s} p_i^{-1}\\right)^{-1} \\mu$$$
Lean4
/-- See `MemLp.prod` for the unapplied version. -/
protected theorem prod' (hf : ∀ i ∈ s, MemLp (f i) (p i) μ) : MemLp (fun ω ↦ ∏ i ∈ s, f i ω) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ :=
by simpa [Finset.prod_fn] using MemLp.prod hf
