aemeasurable_smul_const — Mathlib

English

Let φ: α → F →L[𝕜] E, μ a measure, and c ∈ E with c ≠ 0. Then AEMeasurable (a ↦ φ(a)(c)) μ is equivalent to AEMeasurable (f) μ in the sense described by a similar scalar multiplication relation.

Русский

Пусть φ: α → F →L[𝕜] E, μ — мера, и фиксированно c ∈ E, c ≠ 0. Тогда AEMeasurable(а ↦ φ(a)(c)) по μ эквивалентно AEMeasurable f по μ в рамках аналогичного отношения умножения на константу.

LaTeX

$$$c \\neq 0 \\Rightarrow (\\text{AEMeasurable}(a \\mapsto \\phi(a)(c), μ) \\iff \\text{AEMeasurable}(a \\mapsto \\phi(a), μ)).$$$

Lean4

theorem aemeasurable_smul_const {f : α → 𝕜} {μ : Measure α} {c : E} (hc : c ≠ 0) :
    AEMeasurable (fun x => f x • c) μ ↔ AEMeasurable f μ :=
  (isClosedEmbedding_smul_left hc).measurableEmbedding.aemeasurable_comp_iff

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