mul — Mathlib

English

If f and g are Finite Strongly Measurable, then their product f·g is Finite Strongly Measurable.

Русский

Если f и g финитно сильно измеримы, то их произведение f·g также финитно сильно измеримо.

LaTeX

$$$\text{FinStronglyMeasurable}(f,\mu) \land \text{FinStronglyMeasurable}(g,\mu) \Rightarrow \text{FinStronglyMeasurable}(f \cdot g, \mu)$$$

Lean4

@[aesop safe 20 (rule_sets := [Measurable])]
protected theorem mul [MulZeroClass β] [ContinuousMul β] (hf : FinStronglyMeasurable f μ)
    (hg : FinStronglyMeasurable g μ) : FinStronglyMeasurable (f * g) μ :=
  by
  refine ⟨fun n => hf.approx n * hg.approx n, ?_, fun x => (hf.tendsto_approx x).mul (hg.tendsto_approx x)⟩
  intro n
  exact (measure_mono (support_mul_subset_left _ _)).trans_lt (hf.fin_support_approx n)

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