α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
⊢ HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
⊢ HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
have hb_nonneg : ∀ᵐ a ∂μ, ∀ n, 0 ≤ bound n a :=
  eventually_countable_forall.2 fun n => (h_bound n).mono fun a => (norm_nonneg _).trans
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
⊢ HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
⊢ HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
have hb_le_tsum : ∀ n, bound n ≤ᵐ[μ] fun a => ∑' n, bound n a := by
  intro n
  filter_upwards [hb_nonneg, bound_summable]
    with _ ha0 ha_sum using le_tsum ha_sum _ fun i _ => ha0 i
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n)
⊢ HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
⊢ HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
have hF_integrable : ∀ n, Integrable (F n) μ := by
  refine' fun n => bound_integrable.mono' (hF_meas n) _
  exact EventuallyLE.trans (h_bound n) (hb_le_tsum n)
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n)
⊢ Tendsto (fun s => ∫ (a : α), ∑ i in s, F i a ∂μ) atTop (𝓝 (∫ (a : α), f a ∂μ))
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n)
⊢ HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
simp only [HasSum, ← integral_finset_sum _ fun n _ => hF_integrable n]
case refine'_1
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n)
⊢ ∀ᶠ (n : Finset ι) in atTop, AEStronglyMeasurable (fun a => ∑ i in n, F i a) μ

case refine'_2
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n)
⊢ ∀ᶠ (n : Finset ι) in atTop, ∀ᵐ (a : α) ∂μ, ‖∑ i in n, F i a‖ ≤ (fun a => ∑' (n : ι), bound n a) a
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n)
⊢ Tendsto (fun s => ∫ (a : α), ∑ i in s, F i a ∂μ) atTop (𝓝 (∫ (a : α), f a ∂μ))
refine' tendsto_integral_filter_of_dominated_convergence
    (fun a => ∑' n, bound n a) _ _ bound_integrable h_lim
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
n : ι
⊢ bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
⊢ ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
intro n
no goals
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
n : ι
⊢ bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
filter_upwards [hb_nonneg, bound_summable]
  with _ ha0 ha_sum using le_tsum ha_sum _ fun i _ => ha0 i
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
n : ι
⊢ ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ ∑' (n : ι), bound n a
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
⊢ ∀ (n : ι), Integrable (F n)
refine' fun n => bound_integrable.mono' (hF_meas n) _
no goals
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
n : ι
⊢ ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ ∑' (n : ι), bound n a
exact EventuallyLE.trans (h_bound n) (hb_le_tsum n)
no goals
case refine'_1
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n)
⊢ ∀ᶠ (n : Finset ι) in atTop, AEStronglyMeasurable (fun a => ∑ i in n, F i a) μ
exact eventually_of_forall fun s => s.aestronglyMeasurable_sum fun n _ => hF_meas n
case refine'_2
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n)
s : Finset ι
⊢ ∀ᵐ (a : α) ∂μ, ‖∑ i in s, F i a‖ ≤ (fun a => ∑' (n : ι), bound n a) a
case refine'_2
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n)
⊢ ∀ᶠ (n : Finset ι) in atTop, ∀ᵐ (a : α) ∂μ, ‖∑ i in n, F i a‖ ≤ (fun a => ∑' (n : ι), bound n a) a
refine' eventually_of_forall fun s => _
case h
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n)
s : Finset ι
a : α
hFa : ∀ (i : ι), ‖F i a‖ ≤ bound i a
ha0 : ∀ (n : ι), 0 ≤ bound n a
has : Summable fun n => bound n a
⊢ ‖∑ i in s, F i a‖ ≤ ∑' (n : ι), bound n a
case refine'_2
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n)
s : Finset ι
⊢ ∀ᵐ (a : α) ∂μ, ‖∑ i in s, F i a‖ ≤ (fun a => ∑' (n : ι), bound n a) a
filter_upwards [eventually_countable_forall.2 h_bound, hb_nonneg, bound_summable]
  with a hFa ha0 has
no goals
case h
α : Type u_2
E : Type u_3
F✝ : Type ?u.1002225
𝕜 : Type ?u.1002228
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 α
ι : Type u_1
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable fun a => ∑' (n : ι), bound n a
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n)
s : Finset ι
a : α
hFa : ∀ (i : ι), ‖F i a‖ ≤ bound i a
ha0 : ∀ (n : ι), 0 ≤ bound n a
has : Summable fun n => bound n a
⊢ ‖∑ i in s, F i a‖ ≤ ∑' (n : ι), bound n a
calc
  ‖∑ n in s, F n a‖ ≤ ∑ n in s, bound n a := norm_sum_le_of_le _ fun n _ => hFa n
  _ ≤ ∑' n, bound n a := sum_le_tsum _ (fun n _ => ha0 n) has