smul_measure — Mathlib

English

If f is AEStronglyMeasurable with respect to μ, then for any scalar c, f is AEStronglyMeasurable with respect to the scaled measure c • μ.

Русский

Если f сильно измерима относительно μ, то она остаётся сильно измеримой относительно любого масштаба меры c μ.

LaTeX

$$$\forall c, \; \text{AEStronglyMeasurable}(f, c \cdot μ).$$$

Lean4

@[fun_prop, measurability]
theorem smul_measure {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (h : AEStronglyMeasurable f μ) (c : R) :
    AEStronglyMeasurable f (c • μ) :=
  ⟨h.mk f, h.stronglyMeasurable_mk, ae_smul_measure h.ae_eq_mk c⟩

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