const_smul — Mathlib

English

A constant scalar multiple of a Finite Strongly Measurable function is Finite Strongly Measurable.

Русский

Константное умножение функции, финитно сильно измеримой, сохраняет финитную сильную измеримость.

LaTeX

$$$\forall c, \ FinStronglyMeasurable(f) \Rightarrow \ FinStronglyMeasurable(c \cdot f)$$$

Lean4

@[measurability]
protected theorem const_smul {𝕜} [TopologicalSpace 𝕜] [Zero β] [SMulZeroClass 𝕜 β] [ContinuousSMul 𝕜 β]
    (hf : FinStronglyMeasurable f μ) (c : 𝕜) : FinStronglyMeasurable (c • f) μ :=
  by
  refine ⟨fun n => c • hf.approx n, fun n => ?_, fun x => (hf.tendsto_approx x).const_smul c⟩
  rw [SimpleFunc.coe_smul]
  exact (measure_mono (support_const_smul_subset c _)).trans_lt (hf.fin_support_approx n)

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