-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem hasSum_integral_measure {ι} {m : MeasurableSpace α} {f : α → G} {μ : ι → Measure α}
    (hf : Integrable f (Measure.sum μ)) :
    HasSum (fun i => ∫ a, f a ∂μ i) (∫ a, f a ∂Measure.sum μ)

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ
ε0 : 0 < ε
⊢ ∀ᶠ (x : Finset ι) in atTop, ∫ (a : α), f a ∂∑ i ∈ x, μ i ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ε

Tactic:
lift ε to ℝ≥0 using ε0.le

Result:
case intro
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
⊢ ∀ᶠ (x : Finset ι) in atTop, ∫ (a : α), f a ∂∑ i ∈ x, μ i ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε

Proof state:
case intro
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
⊢ ∀ᶠ (x : Finset ι) in atTop, ∫ (a : α), f a ∂∑ i ∈ x, μ i ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε

Tactic:
have hf_lt : (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ) < ∞ := hf.2

Result:
case intro
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ⊤
⊢ ∀ᶠ (x : Finset ι) in atTop, ∫ (a : α), f a ∂∑ i ∈ x, μ i ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε

Proof state:
case intro.intro
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ⊤
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i => ∫⁻ (a : α), ‖f a‖ₑ ∂μ i) b + ↑ε
ν : Measure α
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ↑(nndist (∫ (a : α), f a ∂∑ i ∈ s, μ i) (∫ (a : α), f a ∂(∑ i ∈ s, μ i + ν))) < ↑ε

Tactic:
rw [← hν, integrable_add_measure] at hf

Result:
case intro.intro
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ⊤
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i => ∫⁻ (a : α), ‖f a‖ₑ ∂μ i) b + ↑ε
ν : Measure α
hf : Integrable f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ↑(nndist (∫ (a : α), f a ∂∑ i ∈ s, μ i) (∫ (a : α), f a ∂(∑ i ∈ s, μ i + ν))) < ↑ε

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ⊤
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i => ∫⁻ (a : α), ‖f a‖ₑ ∂μ i) b + ↑ε
⊢ ∃ ν, ∑ i ∈ s, μ i + ν = Measure.sum μ

Tactic:
refine ⟨Measure.sum fun i : ↥(sᶜ : Set ι) => μ i, ?_⟩

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ⊤
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i => ∫⁻ (a : α), ‖f a‖ₑ ∂μ i) b + ↑ε
⊢ (∑ i ∈ s, μ i + Measure.sum fun i => μ ↑i) = Measure.sum μ

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ⊤
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i => ∫⁻ (a : α), ‖f a‖ₑ ∂μ i) b + ↑ε
⊢ (∑ i ∈ s, μ i + Measure.sum fun i => μ ↑i) = Measure.sum μ

Tactic:
simpa only [← Measure.sum_coe_finset] using Measure.sum_add_sum_compl (s : Set ι) μ

Result:
no goals

Proof state:
case intro
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ⊤
⊢ ∀ᶠ (x : Finset ι) in atTop, ∫ (a : α), f a ∂∑ i ∈ x, μ i ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε

Tactic:
have hmem : ∀ᶠ y in 𝓝 (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ), (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ) < y + ε := by
  refine tendsto_id.add tendsto_const_nhds (lt_mem_nhds (α := ℝ≥0∞) <| ENNReal.lt_add_right ?_ ?_)
  exacts [hf_lt.ne, ENNReal.coe_ne_zero.2 (NNReal.coe_ne_zero.1 ε0.ne')]

Result:
case intro
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ⊤
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
⊢ ∀ᶠ (x : Finset ι) in atTop, ∫ (a : α), f a ∂∑ i ∈ x, μ i ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
⊢ HasSum (fun i => ∫ (a : α), f a ∂μ i) (∫ (a : α), f a ∂Measure.sum μ)

Tactic:
simp only [HasSum, ← integral_finset_sum_measure fun i _ => hfi i]

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
⊢ Tendsto (fun s => ∫ (a : α), f a ∂∑ i ∈ s, μ i) atTop (𝓝 (∫ (a : α), f a ∂Measure.sum μ))

Proof state:
case intro.intro
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < ⊤
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : α), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
ν : Measure α
hs : ∑ i ∈ s, ∫⁻ (a : α), ‖f a‖ₑ ∂μ i + ∫⁻ (a : α), ‖f a‖ₑ ∂ν < ∑ b ∈ s, (fun i => ∫⁻ (a : α), ‖f a‖ₑ ∂μ i) b + ↑ε
hf : Integrable f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂ν < ↑ε

Tactic:
exact lt_of_add_lt_add_left hs

Result:
no goals