mul' — Mathlib

English

Variant of MemLp.mul where the product is written as φ(x) * f(x) instead of φ * f.

Русский

Вариант MemLp.mul, где произведение записано как φ(x) * f(x) вместо φ * f.

LaTeX

$$MemLp (fun x => φ(x) * f x) r μ$$

Lean4

/-- Variant of `MemLp.mul` where the function is written as `fun x ↦ φ x * f x`
instead of `φ * f`. -/
theorem mul' (hf : MemLp f q μ) (hφ : MemLp φ p μ) [hpqr : HolderTriple p q r] : MemLp (fun x ↦ φ x * f x) r μ :=
  MemLp.smul hf hφ

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