case h
α : Type u_2
β : Type ?u.30911
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ (f + g)) i = ↑(withDensityᵥ μ f + withDensityᵥ μ g) i
α : Type u_2
β : Type ?u.30911
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
⊢ withDensityᵥ μ (f + g) = withDensityᵥ μ f + withDensityᵥ μ g
ext1 i hi
case h
α : Type u_2
β : Type ?u.30911
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ (∫ (x : α) in i, (f + g) x ∂μ) = (∫ (x : α) in i, f x ∂μ) + ∫ (x : α) in i, g x ∂μ
case h
α : Type u_2
β : Type ?u.30911
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ (f + g)) i = ↑(withDensityᵥ μ f + withDensityᵥ μ g) i
rw [withDensityᵥ_apply (hf.add hg) hi, VectorMeasure.add_apply, withDensityᵥ_apply hf hi,
  withDensityᵥ_apply hg hi]
case h
α : Type u_2
β : Type ?u.30911
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ (∫ (x : α) in i, f x + g x ∂μ) = (∫ (x : α) in i, f x ∂μ) + ∫ (x : α) in i, g x ∂μ
case h
α : Type u_2
β : Type ?u.30911
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ (∫ (x : α) in i, (f + g) x ∂μ) = (∫ (x : α) in i, f x ∂μ) + ∫ (x : α) in i, g x ∂μ
simp_rw [Pi.add_apply]
case h.hf
α : Type u_2
β : Type ?u.30911
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ IntegrableOn (fun x => f x) Set.univ

case h.hg
α : Type u_2
β : Type ?u.30911
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ IntegrableOn (fun x => g x) Set.univ
case h
α : Type u_2
β : Type ?u.30911
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ (∫ (x : α) in i, f x + g x ∂μ) = (∫ (x : α) in i, f x ∂μ) + ∫ (x : α) in i, g x ∂μ
rw [integral_add] <;> rw [← integrableOn_univ]
no goals
case h.hf
α : Type u_2
β : Type ?u.30911
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ IntegrableOn (fun x => f x) Set.univ
exact hf.integrableOn.restrict MeasurableSet.univ
no goals
case h.hg
α : Type u_2
β : Type ?u.30911
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ IntegrableOn (fun x => g x) Set.univ
exact hg.integrableOn.restrict MeasurableSet.univ