-- 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:
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

Tactic:
exact Pi.summable.mpr fun p => ENNReal.summable

Result:
no goals

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
this : Function.uncurry (∑' (n : ι), f n) = ∑' (n : ι), Function.uncurry (f n)
⊢ Measurable (∑' (n : ι), Function.uncurry (f n))

Tactic:
fun_prop

Result:
no goals

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))
⊢ κ.withDensity (∑' (n : ι), f n) = Kernel.sum fun n => κ.withDensity (f n)

Tactic:
have h_sum_a : ∀ a, Summable fun n => f n a := fun a => Pi.summable.mpr fun b => ENNReal.summable

Result:
α : 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
⊢ κ.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
⊢ κ.withDensity (∑' (n : ι), f n) = Kernel.sum fun n => κ.withDensity (f n)

Tactic:
ext a s hs

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
⊢ ((κ.withDensity (∑' (n : ι), f n)) a) s = ((Kernel.sum fun 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
⊢ ∫⁻ (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))

Tactic:
swap

Result:
α : 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))

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

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
⊢ κ.withDensity (∑' (n : ι), f n) = Kernel.sum fun n => κ.withDensity (f n)

Tactic:
have h_sum : Summable fun n => f n := Pi.summable.mpr h_sum_a

Result:
α : 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
⊢ κ.withDensity (∑' (n : ι), f n) = Kernel.sum fun n => κ.withDensity (f n)

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
⊢ ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∑' (n : ι), ((κ.withDensity (f n)) a) s

Tactic:
have : ∫⁻ b in s, (∑' n, f n) a b ∂κ a = ∫⁻ b in s, ∑' n, (fun b => f n a b) b ∂κ a := by
  congr with b
  rw [tsum_apply h_sum, tsum_apply (h_sum_a a)]

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
⊢ ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∑' (n : ι), ((κ.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
this : Function.uncurry (∑' (n : ι), f n) = ∑' (n : ι), Function.uncurry (f n)
⊢ Measurable (Function.uncurry (∑' (n : ι), f n))

Tactic:
rw [this]

Result:
α : 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 : Function.uncurry (∑' (n : ι), f n) = ∑' (n : ι), Function.uncurry (f n)
⊢ Measurable (∑' (n : ι), Function.uncurry (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
this : ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂κ a
n : ι
⊢ AEMeasurable (fun b => f n a b) ((κ a).restrict s)

Tactic:
fun_prop

Result:
no goals