α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ IsSFiniteKernel (kernel.sum κs)
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
⊢ IsSFiniteKernel (kernel.sum κs)
let e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ kernel.sum κs = kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ IsSFiniteKernel (kernel.sum κs)
refine' ⟨⟨fun n => seq (κs (e n).1) (e n).2, inferInstance, _⟩⟩
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
⊢ kernel.sum κs = kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ kernel.sum κs = kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd
have hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n)) := by
  simp_rw [kernel_sum_seq]
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
⊢ MeasurableSet s → ↑↑(↑(kernel.sum κs) a) s = ↑↑(↑(kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd) a) s
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
⊢ kernel.sum κs = kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd
ext a s
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(kernel.sum κs) a) s = ↑↑(↑(kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd) a) s
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
⊢ MeasurableSet s → ↑↑(↑(kernel.sum κs) a) s = ↑↑(↑(kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd) a) s
intro hs
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(kernel.sum fun n => kernel.sum (seq (κs n))) a) s = ↑↑(↑(kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd) a) s
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(kernel.sum κs) a) s = ↑↑(↑(kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd) a) s
rw [hκ_eq]
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
hs : MeasurableSet s
⊢ (∑' (n : ι) (n_1 : ℕ), ↑↑(↑(seq (κs n) n_1) a) s) =
    ∑' (n : ℕ), ↑↑(↑(seq (κs (↑(Denumerable.eqv (ι × ℕ)).symm n).fst) (↑(Denumerable.eqv (ι × ℕ)).symm n).snd) a) s
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(kernel.sum fun n => kernel.sum (seq (κs n))) a) s = ↑↑(↑(kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd) a) s
simp_rw [kernel.sum_apply' _ _ hs]
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
hs : MeasurableSet s
⊢ (∑' (i : ι) (m : ℕ), ↑↑(↑(seq (κs i) m) a) s) = ∑' (n : ℕ), (fun im => ↑↑(↑(seq (κs im.fst) im.snd) a) s) (↑e n)
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
hs : MeasurableSet s
⊢ (∑' (n : ι) (n_1 : ℕ), ↑↑(↑(seq (κs n) n_1) a) s) =
    ∑' (n : ℕ), ↑↑(↑(seq (κs (↑(Denumerable.eqv (ι × ℕ)).symm n).fst) (↑(Denumerable.eqv (ι × ℕ)).symm n).snd) a) s
change (∑' i, ∑' m, seq (κs i) m a s) = ∑' n, (fun im : ι × ℕ => seq (κs im.fst) im.snd a s) (e n)
no goals
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
hs : MeasurableSet s
⊢ (∑' (i : ι) (m : ℕ), ↑↑(↑(seq (κs i) m) a) s) = ∑' (n : ℕ), (fun im => ↑↑(↑(seq (κs im.fst) im.snd) a) s) (↑e n)
rw [e.tsum_eq (fun im : ι × ℕ => seq (κs im.fst) im.snd a s),
  tsum_prod' ENNReal.summable fun _ => ENNReal.summable]
no goals
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
simp_rw [kernel_sum_seq]