-- Mathlib/Probability/Kernel/WithDensity.lean
theorem withDensity_tsum [Countable ι] (κ : Kernel α β) [IsSFiniteKernel κ] {f : ι → α → β → ℝ≥0∞}
    (hf : ∀ i, Measurable (Function.uncurry (f i))) :
    withDensity κ (∑' n, f n) = Kernel.sum fun n => withDensity κ (f n)

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂κ a

Tactic:
congr with b

Result:
case e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
b : β
⊢ (∑' (n : ι), f n) a b = ∑' (n : ι), (fun b => f n a b) b

Proof state:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
this : ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂κ a
⊢ ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∑' (n : ι), ((κ.withDensity (f n)) a) s

Tactic:
rw [this, lintegral_tsum fun n => by fun_prop]

Result:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
this : ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂κ a
⊢ ∑' (i : ι), ∫⁻ (a_1 : β) in s, f i a a_1 ∂κ a = ∑' (n : ι), ((κ.withDensity (f n)) a) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
this : ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂κ a
⊢ ∑' (i : ι), ∫⁻ (a_1 : β) in s, f i a a_1 ∂κ a = ∑' (n : ι), ((κ.withDensity (f n)) a) s

Tactic:
congr with n

Result:
case h.h.e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
this : ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂κ a
n : ι
⊢ ∫⁻ (a_1 : β) in s, f n a a_1 ∂κ a = ((κ.withDensity (f n)) a) s

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
⊢ Function.uncurry (∑' (n : ι), f n) = ∑' (n : ι), Function.uncurry (f n)

Tactic:
ext1 p

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
⊢ Function.uncurry (∑' (n : ι), f n) p = (∑' (n : ι), Function.uncurry (f n)) p

Proof state:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
⊢ ((κ.withDensity (∑' (n : ι), f n)) a) s = ((Kernel.sum fun n => κ.withDensity (f n)) a) s

Tactic:
rw [sum_apply' _ a hs, Kernel.withDensity_apply' κ _ a s]

Result:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∑' (n : ι), ((κ.withDensity (f n)) a) s

α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable (Function.uncurry (∑' (n : ι), f n))

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
⊢ (∑' (n : ι), f n) p.1 p.2 = (∑' (n : ι), fun p => f n p.1 p.2) p

Tactic:
rw [tsum_apply h_sum, tsum_apply (h_sum_a _), tsum_apply]

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
⊢ Summable fun n p => f n p.1 p.2

Proof state:
case h.h.e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
this : ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂κ a
n : ι
⊢ ∫⁻ (a_1 : β) in s, f n a a_1 ∂κ a = ((κ.withDensity (f n)) a) s

Tactic:
rw [Kernel.withDensity_apply' _ (hf n) a s]

Result:
no goals