aestronglyMeasurable_sum_measure_iff

English

For a PseudoMetrizable β, AEStronglyMeasurable f with respect to the sum of measures μ is equivalent to f being AEStronglyMeasurable with respect to each μ_i individually.

Русский

Для псевдометрического пространства β и функции f, AEStronglyMeasurable относительно суммарной меры μ равносильно тому, что f является AEStronglyMeasurable относительно каждой меры μ_i по отдельности.

LaTeX

$$$\text{AEStronglyMeasurable}(f,\sum_i μ_i) \iff ∀ i,\; \text{AEStronglyMeasurable}(f, μ_i).$$$

Lean4

@[simp]
theorem _root_.aestronglyMeasurable_sum_measure_iff [PseudoMetrizableSpace β] {_m : MeasurableSpace α}
    {μ : ι → Measure α} : AEStronglyMeasurable f (sum μ) ↔ ∀ i, AEStronglyMeasurable f (μ i) :=
  ⟨fun h _ => h.mono_measure (Measure.le_sum _ _), sum_measure⟩

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