integrable_mul — Mathlib

English

If f ∈ Lp and g ∈ Lq with Hölder triple, then f g ∈ L1 (Integrable).

Русский

Если f ∈ L^p и g ∈ L^q с тройной оценкой Холдера, то f g ∈ L^1.

LaTeX

$$$\mathrm{MemLp}(f,p,\mu) \land \mathrm{MemLp}(g,q,\mu) \Rightarrow \mathrm{Integrable}(f \cdot g,\mu).$$$

Lean4

theorem integrable_mul {p q : ℝ≥0∞} {f g : α → 𝕜} (hf : MemLp f p μ) (hg : MemLp g q μ) [HolderTriple p q 1] :
    Integrable (f * g) μ :=
  memLp_one_iff_integrable.1 <| hg.mul hf

Похожие утверждения