coeFn_lpSMul — Mathlib

English

The scalar action on Lp(E,p) and Lp(F,q) corresponds a.e. to the pointwise scalar action on the product f(x)·g(x).

Русский

Действие скаляра на Lp(E,p) и Lp(F,q) соответствует по almost everywhere точечному действию на произведение f(x)·g(x).

LaTeX

$$$\\text{coeFn}_{Lp}(f,g)(x) = f(x) \\cdot g(x) \\quad\\text{a.e.}$$$

Lean4

theorem coeFn_lpSMul (f : Lp 𝕜 p μ) (g : Lp E q μ) : (f • g : Lp E r μ) =ᵐ[μ] ⇑f • g :=
  by
  rw [smul_def]
  exact MemLp.coeFn_toLp _

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