α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
⊢ HasSum (fun i => ∫ (a : α), f a ∂μ i) (∫ (a : α), f a ∂Measure.sum μ)
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
⊢ HasSum (fun i => ∫ (a : α), f a ∂μ i) (∫ (a : α), f a ∂Measure.sum μ)
have hfi : ∀ i, Integrable f (μ i) := fun i => hf.mono_measure (Measure.le_sum _ _)
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
⊢ Tendsto (fun s => ∫ (a : α), f a ∂∑ i in s, μ i) atTop (𝓝 (∫ (a : α), f a ∂Measure.sum μ))
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
⊢ HasSum (fun i => ∫ (a : α), f a ∂μ i) (∫ (a : α), f a ∂Measure.sum μ)
simp only [HasSum, ← integral_finset_sum_measure fun i _ => hfi i]
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ
ε0 : 0 < ε
⊢ ∀ᶠ (x : Finset ι) in atTop, (∫ (a : α), f a ∂∑ i in x, μ i) ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ε
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
⊢ Tendsto (fun s => ∫ (a : α), f a ∂∑ i in s, μ i) atTop (𝓝 (∫ (a : α), f a ∂Measure.sum μ))
refine' Metric.nhds_basis_ball.tendsto_right_iff.mpr fun ε ε0 => _
case intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥0
ε0 : 0 < ↑ε
⊢ ∀ᶠ (x : Finset ι) in atTop, (∫ (a : α), f a ∂∑ i in x, μ i) ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ
ε0 : 0 < ε
⊢ ∀ᶠ (x : Finset ι) in atTop, (∫ (a : α), f a ∂∑ i in x, μ i) ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ε
lift ε to ℝ≥0 using ε0.le
case intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ) < ⊤
⊢ ∀ᶠ (x : Finset ι) in atTop, (∫ (a : α), f a ∂∑ i in x, μ i) ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
case intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥0
ε0 : 0 < ↑ε
⊢ ∀ᶠ (x : Finset ι) in atTop, (∫ (a : α), f a ∂∑ i in x, μ i) ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
have hf_lt : (∫⁻ x, ‖f x‖₊ ∂Measure.sum μ) < ∞ := hf.2
case intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in x, μ i) ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
case intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ) < ⊤
⊢ ∀ᶠ (x : Finset ι) in atTop, (∫ (a : α), f a ∂∑ i in x, μ i) ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
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')]
case intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
⊢ (∫ (a : α), f a ∂∑ i in s, μ i) ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
case intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in x, μ i) ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
refine' ((hasSum_lintegral_measure (fun x => ‖f x‖₊) μ).eventually hmem).mono fun s hs => _
case intro.intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν✝ : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
ν : Measure α
hν : ∑ i in s, μ i + ν = Measure.sum μ
⊢ (∫ (a : α), f a ∂∑ i in s, μ i) ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
case intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
⊢ (∫ (a : α), f a ∂∑ i in s, μ i) ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
obtain ⟨ν, hν⟩ : ∃ ν, (∑ i in s, μ i) + ν = Measure.sum μ := by
  refine' ⟨Measure.sum fun i : ↥(sᶜ : Set ι) => μ i, _⟩
  simpa only [← Measure.sum_coe_finset] using Measure.sum_add_sum_compl (s : Set ι) μ
case intro.intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν✝ : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
ν : Measure α
hν : ∑ i in s, μ i + ν = Measure.sum μ
⊢ ↑(nndist (∫ (a : α), f a ∂∑ i in s, μ i) (∫ (a : α), f a ∂∑ i in s, μ i + ν)) < ↑ε
case intro.intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν✝ : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
ν : Measure α
hν : ∑ i in s, μ i + ν = Measure.sum μ
⊢ (∫ (a : α), f a ∂∑ i in s, μ i) ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
rw [Metric.mem_ball, ← coe_nndist, NNReal.coe_lt_coe, ← ENNReal.coe_lt_coe, ← hν]
case intro.intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν✝ : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
ν : Measure α
hf : Integrable f ∧ Integrable f
hν : ∑ i in s, μ i + ν = Measure.sum μ
⊢ ↑(nndist (∫ (a : α), f a ∂∑ i in s, μ i) (∫ (a : α), f a ∂∑ i in s, μ i + ν)) < ↑ε
case intro.intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν✝ : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
ν : Measure α
hν : ∑ i in s, μ i + ν = Measure.sum μ
⊢ ↑(nndist (∫ (a : α), f a ∂∑ i in s, μ i) (∫ (a : α), f a ∂∑ i in s, μ i + ν)) < ↑ε
rw [← hν, integrable_add_measure] at hf
case intro.intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν✝ : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
ν : Measure α
hf : Integrable f ∧ Integrable f
hν : ∑ i in s, μ i + ν = Measure.sum μ
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ∂ν) < ↑ε
case intro.intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν✝ : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
ν : Measure α
hf : Integrable f ∧ Integrable f
hν : ∑ i in s, μ i + ν = Measure.sum μ
⊢ ↑(nndist (∫ (a : α), f a ∂∑ i in s, μ i) (∫ (a : α), f a ∂∑ i in s, μ i + ν)) < ↑ε
refine' (nndist_integral_add_measure_le_lintegral hf.1 hf.2).trans_lt _
case intro.intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν✝ : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) + ∫⁻ (a : α), ↑‖f a‖₊ ∂ν) < ∑ b in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
hf : Integrable f ∧ Integrable f
hν : ∑ i in s, μ i + ν = Measure.sum μ
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ∂ν) < ↑ε
case intro.intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν✝ : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
ν : Measure α
hf : Integrable f ∧ Integrable f
hν : ∑ i in s, μ i + ν = Measure.sum μ
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ∂ν) < ↑ε
rw [← hν, lintegral_add_measure, lintegral_finset_sum_measure] at hs
no goals
case intro.intro
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν✝ : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) + ∫⁻ (a : α), ↑‖f a‖₊ ∂ν) < ∑ b in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
hf : Integrable f ∧ Integrable f
hν : ∑ i in s, μ i + ν = Measure.sum μ
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ∂ν) < ↑ε
exact lt_of_add_lt_add_left hs
case refine'_1
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ) < ⊤
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ) ≠ ⊤

case refine'_2
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ) < ⊤
⊢ ↑ε ≠ 0
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ) < ⊤
⊢ ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ), (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ) < y + ↑ε
refine' tendsto_id.add tendsto_const_nhds (lt_mem_nhds (α := ℝ≥0∞) <| ENNReal.lt_add_right _ _)
no goals
case refine'_1
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ) < ⊤
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ) ≠ ⊤

case refine'_2
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ) < ⊤
⊢ ↑ε ≠ 0
exacts [hf_lt.ne, ENNReal.coe_ne_zero.2 (NNReal.coe_ne_zero.1 ε0.ne')]
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
⊢ (∑ i in s, μ i + Measure.sum fun i => μ ↑i) = Measure.sum μ
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
⊢ ∃ ν, ∑ i in s, μ i + ν = Measure.sum μ
refine' ⟨Measure.sum fun i : ↥(sᶜ : Set ι) => μ i, _⟩
no goals
α : Type u_2
E : Type u_3
F : Type ?u.1319866
𝕜 : Type ?u.1319869
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m✝ : MeasurableSpace α
μ✝ : Measure α
X : Type ?u.1322560
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
ι : Type u_1
m : MeasurableSpace α
f : α → E
μ : ι → Measure α
hf : Integrable f
hfi : ∀ (i : ι), Integrable f
ε : ℝ≥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 in s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε
⊢ (∑ i in s, μ i + Measure.sum fun i => μ ↑i) = Measure.sum μ
simpa only [← Measure.sum_coe_finset] using Measure.sum_add_sum_compl (s : Set ι) μ