smul — Mathlib

English

If f: α → 𝕜 and g: α → β are AEStronglyMeasurable, then the pointwise product f(x) • g(x) is AEStronglyMeasurable.

Русский

Если f: α → 𝕜 и g: α → β являются AEStronglyMeasurable, то точечное умножение f(x) • g(x) является AEStronglyMeasurable.

LaTeX

$$$AEStronglyMeasurable\ f μ \rightarrow AEStronglyMeasurable\ g μ \rightarrow AEStronglyMeasurable\left( x \mapsto f(x) \; \bullet \; g(x) \right) μ$$$

Lean4

@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
protected theorem smul {𝕜} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜} {g : α → β}
    (hf : AEStronglyMeasurable[m] f μ) (hg : AEStronglyMeasurable[m] g μ) :
    AEStronglyMeasurable[m] (fun x => f x • g x) μ :=
  continuous_smul.comp_aestronglyMeasurable (hf.prodMk hg)

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