English
Let μ_i be measures on X and μ = ∑ μ_i. If S is null-measurable with respect to μ, then the equality of measures holds on S: (∑ μ_i)(S) = ∑ μ_i(S).
Русский
Пусть μ_i — меры на X, и μ = ∑ μ_i. Если S является нулевоизмеримым относительно μ, то выполняется (∑ μ_i)(S) = ∑ μ_i(S).
LaTeX
$$$ (\sum_i μ_i)(S) = \sum_i μ_i(S) \quad \text{при условии } S \text{ нулевоизмеримо относительно } \sum_i μ_i $$$
Lean4
theorem sum_apply₀ (f : ι → Measure α) {s : Set α} (hs : NullMeasurableSet s (sum f)) : sum f s = ∑' i, f i s :=
by
apply le_antisymm ?_ (le_sum_apply _ _)
rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, t_meas, ht⟩
calc
sum f s = sum f t := measure_congr ht.symm
_ = ∑' i, f i t := (sum_apply _ t_meas)
_ ≤ ∑' i, f i s := ENNReal.tsum_le_tsum fun i ↦ measure_mono ts
