α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
⊢ (∑' (i : β), ∫⁻ (a : α) in s i, ↑‖f a‖₊ ∂μ) < ⊤
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
⊢ IntegrableOn f (iUnion s)
refine' ⟨AEStronglyMeasurable.iUnion fun i => (hi i).1, (lintegral_iUnion_le _ _).trans_lt _⟩
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
B : ∀ (b : β), (∫⁻ (a : α) in s b, ↑‖f a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)
⊢ (∑' (i : β), ∫⁻ (a : α) in s i, ↑‖f a‖₊ ∂μ) < ⊤
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
⊢ (∑' (i : β), ∫⁻ (a : α) in s i, ↑‖f a‖₊ ∂μ) < ⊤
have B := fun b : β => lintegral_coe_eq_integral (fun a : α => ‖f a‖₊) (hi b).norm
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
B : ∀ (b : β), (∫⁻ (a : α) in s b, ↑‖f a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)
⊢ (∑' (b : β), ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)) < ⊤
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
B : ∀ (b : β), (∫⁻ (a : α) in s b, ↑‖f a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)
⊢ (∑' (i : β), ∫⁻ (a : α) in s i, ↑‖f a‖₊ ∂μ) < ⊤
rw [tsum_congr B]
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
B : ∀ (b : β), (∫⁻ (a : α) in s b, ↑‖f a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)
S' : Summable fun b => { val := ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ, property := (_ : 0 ≤ ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ) }
⊢ (∑' (b : β), ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)) < ⊤
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
B : ∀ (b : β), (∫⁻ (a : α) in s b, ↑‖f a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)
⊢ (∑' (b : β), ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)) < ⊤
have S' :
  Summable fun b : β =>
    (⟨∫ a : α in s b, ‖f a‖₊ ∂μ, set_integral_nonneg (hs b) fun a _ => NNReal.coe_nonneg _⟩ :
      NNReal) :=
  by rw [← NNReal.summable_coe]; exact h
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
B : ∀ (b : β), (∫⁻ (a : α) in s b, ↑‖f a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)
S' : Summable fun b => { val := ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ, property := (_ : 0 ≤ ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ) }
S'' :
  (∑' (a : β), ↑{ val := ∫ (a : α) in s a, ↑‖f a‖₊ ∂μ, property := (_ : 0 ≤ ∫ (a : α) in s a, ↑‖f a‖₊ ∂μ) }) =
    ↑(∑' (b : β), { val := ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ, property := (_ : 0 ≤ ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ) })
⊢ (∑' (b : β), ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)) < ⊤
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
B : ∀ (b : β), (∫⁻ (a : α) in s b, ↑‖f a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)
S' : Summable fun b => { val := ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ, property := (_ : 0 ≤ ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ) }
⊢ (∑' (b : β), ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)) < ⊤
have S'' := ENNReal.tsum_coe_eq S'.hasSum
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
B : ∀ (b : β), (∫⁻ (a : α) in s b, ↑‖f a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)
S' : Summable fun b => { val := ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ, property := (_ : 0 ≤ ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ) }
S'' :
  (∑' (a : β), ENNReal.ofReal (∫ (a : α) in s a, ‖f a‖ ∂μ)) =
    ENNReal.ofReal
      ↑(∑' (b : β),
          { val := ∫ (a : α) in s b, ‖f a‖ ∂μ, property := (_ : (fun r => 0 ≤ r) (∫ (a : α) in s b, ‖f a‖ ∂μ)) })
⊢ (∑' (b : β), ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)) < ⊤
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
B : ∀ (b : β), (∫⁻ (a : α) in s b, ↑‖f a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)
S' : Summable fun b => { val := ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ, property := (_ : 0 ≤ ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ) }
S'' :
  (∑' (a : β), ↑{ val := ∫ (a : α) in s a, ↑‖f a‖₊ ∂μ, property := (_ : 0 ≤ ∫ (a : α) in s a, ↑‖f a‖₊ ∂μ) }) =
    ↑(∑' (b : β), { val := ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ, property := (_ : 0 ≤ ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ) })
⊢ (∑' (b : β), ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)) < ⊤
simp_rw [ENNReal.coe_nnreal_eq, NNReal.coe_mk, coe_nnnorm] at S''
no goals
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
B : ∀ (b : β), (∫⁻ (a : α) in s b, ↑‖f a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)
S' : Summable fun b => { val := ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ, property := (_ : 0 ≤ ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ) }
S'' :
  (∑' (a : β), ENNReal.ofReal (∫ (a : α) in s a, ‖f a‖ ∂μ)) =
    ENNReal.ofReal
      ↑(∑' (b : β),
          { val := ∫ (a : α) in s b, ‖f a‖ ∂μ, property := (_ : (fun r => 0 ≤ r) (∫ (a : α) in s b, ‖f a‖ ∂μ)) })
⊢ (∑' (b : β), ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)) < ⊤
convert ENNReal.ofReal_lt_top
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
B : ∀ (b : β), (∫⁻ (a : α) in s b, ↑‖f a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)
⊢ Summable fun a => ↑{ val := ∫ (a : α) in s a, ↑‖f a‖₊ ∂μ, property := (_ : 0 ≤ ∫ (a : α) in s a, ↑‖f a‖₊ ∂μ) }
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
B : ∀ (b : β), (∫⁻ (a : α) in s b, ↑‖f a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)
⊢ Summable fun b => { val := ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ, property := (_ : 0 ≤ ∫ (a : α) in s b, ↑‖f a‖₊ ∂μ) }
rw [← NNReal.summable_coe]
no goals
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.299502
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : Countable β
f : α → E
s : β → Set α
hs : ∀ (b : β), MeasurableSet (s b)
hi : ∀ (b : β), IntegrableOn f (s b)
h : Summable fun b => ∫ (a : α) in s b, ‖f a‖ ∂μ
B : ∀ (b : β), (∫⁻ (a : α) in s b, ↑‖f a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α) in s b, ↑‖f a‖₊ ∂μ)
⊢ Summable fun a => ↑{ val := ∫ (a : α) in s a, ↑‖f a‖₊ ∂μ, property := (_ : 0 ≤ ∫ (a : α) in s a, ↑‖f a‖₊ ∂μ) }
exact h