English
If f is AEStronglyMeasurable with respect to each μ_i in a family (i ∈ ι), then f is AEStronglyMeasurable with respect to the sum measure sum μ.
Русский
Если для каждого i функция f является AEStronglyMeasurable относительно меры μ_i, то она также AEStronglyMeasurable относительно суммы мер Σ_i μ_i.
LaTeX
$$$\forall i,\; \text{AEStronglyMeasurable}(f,\mu_i) \Rightarrow \text{AEStronglyMeasurable}(f,\sum_i \mu_i).$$$
Lean4
@[fun_prop]
theorem sum_measure [PseudoMetrizableSpace β] {m : MeasurableSpace α} {μ : ι → Measure α}
(h : ∀ i, AEStronglyMeasurable f (μ i)) : AEStronglyMeasurable f (Measure.sum μ) :=
by
borelize β
refine aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨AEMeasurable.sum_measure fun i => (h i).aemeasurable, ?_⟩
have A : ∀ i : ι, ∃ t : Set β, IsSeparable t ∧ f ⁻¹' t ∈ ae (μ i) := fun i =>
(aestronglyMeasurable_iff_aemeasurable_separable.1 (h i)).2
choose t t_sep ht using A
refine ⟨⋃ i, t i, .iUnion t_sep, ?_⟩
simp only [Measure.ae_sum_eq, mem_iUnion, eventually_iSup]
intro i
filter_upwards [ht i] with x hx
exact ⟨i, hx⟩
