English
Let f: α → G be integrable with respect to two measures μ and ν. Then the Bochner integral with respect to the sum μ + ν equals the sum of the integrals with respect to μ and ν: ∫ f d(μ+ν) = ∫ f dμ + ∫ f dν.
Русский
Пусть f:α→G интегрируема по измерениям μ и ν. Тогда интеграл Боунхер по сумме мер μ+ν равен сумме интегралов по μ и ν: ∫ f d(μ+ν) = ∫ f dμ + ∫ f dν.
LaTeX
$$$$\int x, f(x) \partial(\mu+\nu) = \int x, f(x) \partial\mu + \int x, f(x) \partial\nu.$$$$
Lean4
theorem integral_add_measure {f : α → G} (hμ : Integrable f μ) (hν : Integrable f ν) :
∫ x, f x ∂(μ + ν) = ∫ x, f x ∂μ + ∫ x, f x ∂ν :=
by
by_cases hG : CompleteSpace G; swap
· simp [integral, hG]
have hfi := hμ.add_measure hν
simp_rw [integral_eq_setToFun]
have hμ_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul μ : Set α → G →L[ℝ] G) 1 :=
DominatedFinMeasAdditive.add_measure_right μ ν (dominatedFinMeasAdditive_weightedSMul μ) zero_le_one
have hν_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul ν : Set α → G →L[ℝ] G) 1 :=
DominatedFinMeasAdditive.add_measure_left μ ν (dominatedFinMeasAdditive_weightedSMul ν) zero_le_one
rw [← setToFun_congr_measure_of_add_right hμ_dfma (dominatedFinMeasAdditive_weightedSMul μ) f hfi, ←
setToFun_congr_measure_of_add_left hν_dfma (dominatedFinMeasAdditive_weightedSMul ν) f hfi]
refine setToFun_add_left' _ _ _ (fun s _ hμνs => ?_) f
rw [Measure.coe_add, Pi.add_apply, add_lt_top] at hμνs
rw [weightedSMul, weightedSMul, weightedSMul, ← add_smul, measureReal_add_apply hμνs.1.ne hμνs.2.ne]
