case h
α : Type u_1
β : Type ?u.1767013
γ : Type ?u.1767016
δ : Type ?u.1767019
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
h : ∀ (i : ℕ), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity μ (∑' (n : ℕ), f n)) s = ↑↑(sum fun n => withDensity μ (f n)) s
α : Type u_1
β : Type ?u.1767013
γ : Type ?u.1767016
δ : Type ?u.1767019
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
h : ∀ (i : ℕ), Measurable (f i)
⊢ withDensity μ (∑' (n : ℕ), f n) = sum fun n => withDensity μ (f n)
ext1 s hs
case h
α : Type u_1
β : Type ?u.1767013
γ : Type ?u.1767016
δ : Type ?u.1767019
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
h : ∀ (i : ℕ), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, tsum (fun n => f n) a ∂μ) = ∑' (i : ℕ), ∫⁻ (a : α) in s, f i a ∂μ
case h
α : Type u_1
β : Type ?u.1767013
γ : Type ?u.1767016
δ : Type ?u.1767019
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
h : ∀ (i : ℕ), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity μ (∑' (n : ℕ), f n)) s = ↑↑(sum fun n => withDensity μ (f n)) s
simp_rw [sum_apply _ hs, withDensity_apply _ hs]
case h
α : Type u_1
β : Type ?u.1767013
γ : Type ?u.1767016
δ : Type ?u.1767019
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
h : ∀ (i : ℕ), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (x : α) in s, tsum (fun n => f n) x ∂μ) = ∑' (i : ℕ), ∫⁻ (x : α) in s, f i x ∂μ
case h
α : Type u_1
β : Type ?u.1767013
γ : Type ?u.1767016
δ : Type ?u.1767019
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
h : ∀ (i : ℕ), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, tsum (fun n => f n) a ∂μ) = ∑' (i : ℕ), ∫⁻ (a : α) in s, f i a ∂μ
change (∫⁻ x in s, (∑' n, f n) x ∂μ) = ∑' i : ℕ, ∫⁻ x, f i x ∂μ.restrict s
case h
α : Type u_1
β : Type ?u.1767013
γ : Type ?u.1767016
δ : Type ?u.1767019
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
h : ∀ (i : ℕ), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (x : α) in s, tsum (fun n => f n) x ∂μ) = ∫⁻ (a : α) in s, ∑' (i : ℕ), f i a ∂μ
case h
α : Type u_1
β : Type ?u.1767013
γ : Type ?u.1767016
δ : Type ?u.1767019
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
h : ∀ (i : ℕ), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (x : α) in s, tsum (fun n => f n) x ∂μ) = ∑' (i : ℕ), ∫⁻ (x : α) in s, f i x ∂μ
rw [← lintegral_tsum fun i => (h i).aemeasurable]
no goals
case h
α : Type u_1
β : Type ?u.1767013
γ : Type ?u.1767016
δ : Type ?u.1767019
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
h : ∀ (i : ℕ), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (x : α) in s, tsum (fun n => f n) x ∂μ) = ∫⁻ (a : α) in s, ∑' (i : ℕ), f i a ∂μ
refine' lintegral_congr fun x => tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)