aestronglyMeasurable_smul_const_iff

English

Multiplication by a nonzero scalar preserves AEStronglyMeasurable on functions to a vector space.

Русский

Умножение на ненулевой скаляр сохраняет AEStronglyMeasurable.

LaTeX

$$$$\\text{AEStronglyMeasurable}(f \\cdot c) \\iff \\text{AEStronglyMeasurable}(f)$$ for all nonzero c.$$

Lean4

theorem aestronglyMeasurable_smul_const_iff {f : α → 𝕜} {c : E} (hc : c ≠ 0) :
    AEStronglyMeasurable (fun x => f x • c) μ ↔ AEStronglyMeasurable f μ :=
  (isClosedEmbedding_smul_left hc).isEmbedding.aestronglyMeasurable_comp_iff

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