[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
⊢ Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)
[PROOFSTEP]
refine'
  MeasurableSpace.induction_on_inter (C := fun t => Measurable fun a => κ a (Prod.mk a ⁻¹' t)) generateFrom_prod.symm
    isPiSystem_prod _ _ _ _ ht
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
⊢ (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) ∅
[PROOFSTEP]
simp only [preimage_empty, measure_empty, measurable_const]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
⊢ ∀ (t : Set (α × β)),
    t ∈ image2 (fun x x_1 => x ×ˢ x_1) {s | MeasurableSet s} {t | MeasurableSet t} →
      (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) t
[PROOFSTEP]
intro t' ht'
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : t' ∈ image2 (fun x x_1 => x ×ˢ x_1) {s | MeasurableSet s} {t | MeasurableSet t}
⊢ Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
[PROOFSTEP]
simp only [Set.mem_image2, Set.mem_setOf_eq, exists_and_left] at ht'
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : ∃ a, MeasurableSet a ∧ ∃ x, MeasurableSet x ∧ a ×ˢ x = t'
⊢ Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
[PROOFSTEP]
obtain ⟨t₁, ht₁, t₂, ht₂, rfl⟩ := ht'
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)
[PROOFSTEP]
classical
simp_rw [mk_preimage_prod_right_eq_if]
have h_eq_ite : (fun a => κ a (ite (a ∈ t₁) t₂ ∅)) = fun a => ite (a ∈ t₁) (κ a t₂) 0 :=
  by
  ext1 a
  split_ifs
  exacts [rfl, measure_empty]
rw [h_eq_ite]
exact Measurable.ite ht₁ (kernel.measurable_coe κ ht₂) measurable_const
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)
[PROOFSTEP]
simp_rw [mk_preimage_prod_right_eq_if]
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Measurable fun a => ↑↑(↑κ a) (if a ∈ t₁ then t₂ else ∅)
[PROOFSTEP]
have h_eq_ite : (fun a => κ a (ite (a ∈ t₁) t₂ ∅)) = fun a => ite (a ∈ t₁) (κ a t₂) 0 :=
  by
  ext1 a
  split_ifs
  exacts [rfl, measure_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ (fun a => ↑↑(↑κ a) (if a ∈ t₁ then t₂ else ∅)) = fun a => if a ∈ t₁ then ↑↑(↑κ a) t₂ else 0
[PROOFSTEP]
ext1 a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
⊢ ↑↑(↑κ a) (if a ∈ t₁ then t₂ else ∅) = if a ∈ t₁ then ↑↑(↑κ a) t₂ else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
h✝ : a ∈ t₁
⊢ ↑↑(↑κ a) t₂ = ↑↑(↑κ a) t₂
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
h✝ : ¬a ∈ t₁
⊢ ↑↑(↑κ a) ∅ = 0
[PROOFSTEP]
exacts [rfl, measure_empty]
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
h_eq_ite : (fun a => ↑↑(↑κ a) (if a ∈ t₁ then t₂ else ∅)) = fun a => if a ∈ t₁ then ↑↑(↑κ a) t₂ else 0
⊢ Measurable fun a => ↑↑(↑κ a) (if a ∈ t₁ then t₂ else ∅)
[PROOFSTEP]
rw [h_eq_ite]
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
h_eq_ite : (fun a => ↑↑(↑κ a) (if a ∈ t₁ then t₂ else ∅)) = fun a => if a ∈ t₁ then ↑↑(↑κ a) t₂ else 0
⊢ Measurable fun a => if a ∈ t₁ then ↑↑(↑κ a) t₂ else 0
[PROOFSTEP]
exact Measurable.ite ht₁ (kernel.measurable_coe κ ht₂) measurable_const
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
⊢ ∀ (t : Set (α × β)),
    MeasurableSet t →
      (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) t →
        (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) tᶜ
[PROOFSTEP]
intro t' ht' h_meas
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : MeasurableSet t'
h_meas : Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
⊢ Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t'ᶜ)
[PROOFSTEP]
have h_eq_sdiff : ∀ a, Prod.mk a ⁻¹' t'ᶜ = Set.univ \ Prod.mk a ⁻¹' t' :=
  by
  intro a
  ext1 b
  simp only [mem_compl_iff, mem_preimage, mem_diff, mem_univ, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : MeasurableSet t'
h_meas : Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
⊢ ∀ (a : α), Prod.mk a ⁻¹' t'ᶜ = univ \ Prod.mk a ⁻¹' t'
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : MeasurableSet t'
h_meas : Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
a : α
⊢ Prod.mk a ⁻¹' t'ᶜ = univ \ Prod.mk a ⁻¹' t'
[PROOFSTEP]
ext1 b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : MeasurableSet t'
h_meas : Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
a : α
b : β
⊢ b ∈ Prod.mk a ⁻¹' t'ᶜ ↔ b ∈ univ \ Prod.mk a ⁻¹' t'
[PROOFSTEP]
simp only [mem_compl_iff, mem_preimage, mem_diff, mem_univ, true_and_iff]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : MeasurableSet t'
h_meas : Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' t'ᶜ = univ \ Prod.mk a ⁻¹' t'
⊢ Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t'ᶜ)
[PROOFSTEP]
simp_rw [h_eq_sdiff]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : MeasurableSet t'
h_meas : Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' t'ᶜ = univ \ Prod.mk a ⁻¹' t'
⊢ Measurable fun a => ↑↑(↑κ a) (univ \ Prod.mk a ⁻¹' t')
[PROOFSTEP]
have : (fun a => κ a (Set.univ \ Prod.mk a ⁻¹' t')) = fun a => κ a Set.univ - κ a (Prod.mk a ⁻¹' t') :=
  by
  ext1 a
  rw [← Set.diff_inter_self_eq_diff, Set.inter_univ, measure_diff (Set.subset_univ _)]
  · exact (@measurable_prod_mk_left α β _ _ a) ht'
  · exact measure_ne_top _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : MeasurableSet t'
h_meas : Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' t'ᶜ = univ \ Prod.mk a ⁻¹' t'
⊢ (fun a => ↑↑(↑κ a) (univ \ Prod.mk a ⁻¹' t')) = fun a => ↑↑(↑κ a) univ - ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
[PROOFSTEP]
ext1 a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : MeasurableSet t'
h_meas : Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' t'ᶜ = univ \ Prod.mk a ⁻¹' t'
a : α
⊢ ↑↑(↑κ a) (univ \ Prod.mk a ⁻¹' t') = ↑↑(↑κ a) univ - ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
[PROOFSTEP]
rw [← Set.diff_inter_self_eq_diff, Set.inter_univ, measure_diff (Set.subset_univ _)]
[GOAL]
case h.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : MeasurableSet t'
h_meas : Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' t'ᶜ = univ \ Prod.mk a ⁻¹' t'
a : α
⊢ MeasurableSet (Prod.mk a ⁻¹' t')
[PROOFSTEP]
exact (@measurable_prod_mk_left α β _ _ a) ht'
[GOAL]
case h.h_fin
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : MeasurableSet t'
h_meas : Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' t'ᶜ = univ \ Prod.mk a ⁻¹' t'
a : α
⊢ ↑↑(↑κ a) (Prod.mk a ⁻¹' t') ≠ ⊤
[PROOFSTEP]
exact measure_ne_top _ _
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : MeasurableSet t'
h_meas : Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' t'ᶜ = univ \ Prod.mk a ⁻¹' t'
this : (fun a => ↑↑(↑κ a) (univ \ Prod.mk a ⁻¹' t')) = fun a => ↑↑(↑κ a) univ - ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
⊢ Measurable fun a => ↑↑(↑κ a) (univ \ Prod.mk a ⁻¹' t')
[PROOFSTEP]
rw [this]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
t' : Set (α × β)
ht' : MeasurableSet t'
h_meas : Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' t'ᶜ = univ \ Prod.mk a ⁻¹' t'
this : (fun a => ↑↑(↑κ a) (univ \ Prod.mk a ⁻¹' t')) = fun a => ↑↑(↑κ a) univ - ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
⊢ Measurable fun a => ↑↑(↑κ a) univ - ↑↑(↑κ a) (Prod.mk a ⁻¹' t')
[PROOFSTEP]
exact Measurable.sub (kernel.measurable_coe κ MeasurableSet.univ) h_meas
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
⊢ ∀ (f : ℕ → Set (α × β)),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)) →
          (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (⋃ (i : ℕ), f i)
[PROOFSTEP]
intro f h_disj hf_meas hf
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
⊢ Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)
[PROOFSTEP]
have h_Union : (fun a => κ a (Prod.mk a ⁻¹' ⋃ i, f i)) = fun a => κ a (⋃ i, Prod.mk a ⁻¹' f i) :=
  by
  ext1 a
  congr with b
  simp only [mem_iUnion, mem_preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
⊢ (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
[PROOFSTEP]
ext1 a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
a : α
⊢ ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i) = ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
[PROOFSTEP]
congr with b
[GOAL]
case h.e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
a : α
b : β
⊢ b ∈ Prod.mk a ⁻¹' ⋃ (i : ℕ), f i ↔ b ∈ ⋃ (i : ℕ), Prod.mk a ⁻¹' f i
[PROOFSTEP]
simp only [mem_iUnion, mem_preimage]
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
⊢ Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)
[PROOFSTEP]
rw [h_Union]
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
⊢ Measurable fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
[PROOFSTEP]
have h_tsum : (fun a => κ a (⋃ i, Prod.mk a ⁻¹' f i)) = fun a => ∑' i, κ a (Prod.mk a ⁻¹' f i) :=
  by
  ext1 a
  rw [measure_iUnion]
  · intro i j hij s hsi hsj b hbs
    have habi : {(a, b)} ⊆ f i := by rw [Set.singleton_subset_iff]; exact hsi hbs
    have habj : {(a, b)} ⊆ f j := by rw [Set.singleton_subset_iff]; exact hsj hbs
    simpa only [Set.bot_eq_empty, Set.le_eq_subset, Set.singleton_subset_iff, Set.mem_empty_iff_false] using
      h_disj hij habi habj
  · exact fun i => (@measurable_prod_mk_left α β _ _ a) (hf_meas i)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
⊢ (fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)) = fun a => ∑' (i : ℕ), ↑↑(↑κ a) (Prod.mk a ⁻¹' f i)
[PROOFSTEP]
ext1 a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
a : α
⊢ ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i) = ∑' (i : ℕ), ↑↑(↑κ a) (Prod.mk a ⁻¹' f i)
[PROOFSTEP]
rw [measure_iUnion]
[GOAL]
case h.hn
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
a : α
⊢ Pairwise (Disjoint on fun i => Prod.mk a ⁻¹' f i)
[PROOFSTEP]
intro i j hij s hsi hsj b hbs
[GOAL]
case h.hn
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
a : α
i j : ℕ
hij : i ≠ j
s : Set β
hsi : s ≤ (fun i => Prod.mk a ⁻¹' f i) i
hsj : s ≤ (fun i => Prod.mk a ⁻¹' f i) j
b : β
hbs : b ∈ s
⊢ b ∈ ⊥
[PROOFSTEP]
have habi : {(a, b)} ⊆ f i := by rw [Set.singleton_subset_iff]; exact hsi hbs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
a : α
i j : ℕ
hij : i ≠ j
s : Set β
hsi : s ≤ (fun i => Prod.mk a ⁻¹' f i) i
hsj : s ≤ (fun i => Prod.mk a ⁻¹' f i) j
b : β
hbs : b ∈ s
⊢ {(a, b)} ⊆ f i
[PROOFSTEP]
rw [Set.singleton_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
a : α
i j : ℕ
hij : i ≠ j
s : Set β
hsi : s ≤ (fun i => Prod.mk a ⁻¹' f i) i
hsj : s ≤ (fun i => Prod.mk a ⁻¹' f i) j
b : β
hbs : b ∈ s
⊢ (a, b) ∈ f i
[PROOFSTEP]
exact hsi hbs
[GOAL]
case h.hn
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
a : α
i j : ℕ
hij : i ≠ j
s : Set β
hsi : s ≤ (fun i => Prod.mk a ⁻¹' f i) i
hsj : s ≤ (fun i => Prod.mk a ⁻¹' f i) j
b : β
hbs : b ∈ s
habi : {(a, b)} ⊆ f i
⊢ b ∈ ⊥
[PROOFSTEP]
have habj : {(a, b)} ⊆ f j := by rw [Set.singleton_subset_iff]; exact hsj hbs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
a : α
i j : ℕ
hij : i ≠ j
s : Set β
hsi : s ≤ (fun i => Prod.mk a ⁻¹' f i) i
hsj : s ≤ (fun i => Prod.mk a ⁻¹' f i) j
b : β
hbs : b ∈ s
habi : {(a, b)} ⊆ f i
⊢ {(a, b)} ⊆ f j
[PROOFSTEP]
rw [Set.singleton_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
a : α
i j : ℕ
hij : i ≠ j
s : Set β
hsi : s ≤ (fun i => Prod.mk a ⁻¹' f i) i
hsj : s ≤ (fun i => Prod.mk a ⁻¹' f i) j
b : β
hbs : b ∈ s
habi : {(a, b)} ⊆ f i
⊢ (a, b) ∈ f j
[PROOFSTEP]
exact hsj hbs
[GOAL]
case h.hn
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
a : α
i j : ℕ
hij : i ≠ j
s : Set β
hsi : s ≤ (fun i => Prod.mk a ⁻¹' f i) i
hsj : s ≤ (fun i => Prod.mk a ⁻¹' f i) j
b : β
hbs : b ∈ s
habi : {(a, b)} ⊆ f i
habj : {(a, b)} ⊆ f j
⊢ b ∈ ⊥
[PROOFSTEP]
simpa only [Set.bot_eq_empty, Set.le_eq_subset, Set.singleton_subset_iff, Set.mem_empty_iff_false] using
  h_disj hij habi habj
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
a : α
⊢ ∀ (i : ℕ), MeasurableSet (Prod.mk a ⁻¹' f i)
[PROOFSTEP]
exact fun i => (@measurable_prod_mk_left α β _ _ a) (hf_meas i)
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
h_tsum : (fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)) = fun a => ∑' (i : ℕ), ↑↑(↑κ a) (Prod.mk a ⁻¹' f i)
⊢ Measurable fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
[PROOFSTEP]
rw [h_tsum]
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure (↑κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), (fun t => Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)) (f i)
h_Union : (fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)) = fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)
h_tsum : (fun a => ↑↑(↑κ a) (⋃ (i : ℕ), Prod.mk a ⁻¹' f i)) = fun a => ∑' (i : ℕ), ↑↑(↑κ a) (Prod.mk a ⁻¹' f i)
⊢ Measurable fun a => ∑' (i : ℕ), ↑↑(↑κ a) (Prod.mk a ⁻¹' f i)
[PROOFSTEP]
exact Measurable.ennreal_tsum hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable fun a => ↑↑(↑κ a) (Prod.mk a ⁻¹' t)
[PROOFSTEP]
rw [← kernel.kernel_sum_seq κ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable fun a => ↑↑(↑(kernel.sum (seq κ)) a) (Prod.mk a ⁻¹' t)
[PROOFSTEP]
have : ∀ a, kernel.sum (kernel.seq κ) a (Prod.mk a ⁻¹' t) = ∑' n, kernel.seq κ n a (Prod.mk a ⁻¹' t) := fun a =>
  kernel.sum_apply' _ _ (measurable_prod_mk_left ht)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
this : ∀ (a : α), ↑↑(↑(kernel.sum (seq κ)) a) (Prod.mk a ⁻¹' t) = ∑' (n : ℕ), ↑↑(↑(seq κ n) a) (Prod.mk a ⁻¹' t)
⊢ Measurable fun a => ↑↑(↑(kernel.sum (seq κ)) a) (Prod.mk a ⁻¹' t)
[PROOFSTEP]
simp_rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
this : ∀ (a : α), ↑↑(↑(kernel.sum (seq κ)) a) (Prod.mk a ⁻¹' t) = ∑' (n : ℕ), ↑↑(↑(seq κ n) a) (Prod.mk a ⁻¹' t)
⊢ Measurable fun a => ∑' (n : ℕ), ↑↑(↑(seq κ n) a) (Prod.mk a ⁻¹' t)
[PROOFSTEP]
refine' Measurable.ennreal_tsum fun n => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
this : ∀ (a : α), ↑↑(↑(kernel.sum (seq κ)) a) (Prod.mk a ⁻¹' t) = ∑' (n : ℕ), ↑↑(↑(seq κ n) a) (Prod.mk a ⁻¹' t)
n : ℕ
⊢ Measurable fun a => ↑↑(↑(seq κ n) a) (Prod.mk a ⁻¹' t)
[PROOFSTEP]
exact measurable_kernel_prod_mk_left_of_finite ht inferInstance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
inst✝ : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
⊢ Measurable fun b => ↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s)
[PROOFSTEP]
have : ∀ b, Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p : (α × β) × γ | (p.1.2, p.2) ∈ s}} := by intro b; rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
inst✝ : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
⊢ ∀ (b : β), Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.fst.snd, p.snd) ∈ s}}
[PROOFSTEP]
intro b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
inst✝ : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
b : β
⊢ Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.fst.snd, p.snd) ∈ s}}
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
inst✝ : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this : ∀ (b : β), Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.fst.snd, p.snd) ∈ s}}
⊢ Measurable fun b => ↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s)
[PROOFSTEP]
simp_rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
inst✝ : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this : ∀ (b : β), Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.fst.snd, p.snd) ∈ s}}
⊢ Measurable fun b => ↑↑(↑η (a, b)) {c | ((a, b), c) ∈ {p | (p.fst.snd, p.snd) ∈ s}}
[PROOFSTEP]
refine' (measurable_kernel_prod_mk_left _).comp measurable_prod_mk_left
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
inst✝ : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this : ∀ (b : β), Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.fst.snd, p.snd) ∈ s}}
⊢ MeasurableSet {p | (p.fst.snd, p.snd) ∈ s}
[PROOFSTEP]
exact (measurable_fst.snd.prod_mk measurable_snd) hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable fun a => ∫⁻ (b : β), indicator t (Function.const (α × β) c) (a, b) ∂↑κ a
[PROOFSTEP]
conv =>
  congr
  ext
  erw [lintegral_indicator_const_comp measurable_prod_mk_left ht _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
| Measurable fun a => ∫⁻ (b : β), indicator t (Function.const (α × β) c) (a, b) ∂↑κ a
[PROOFSTEP]
  congr
  ext
  erw [lintegral_indicator_const_comp measurable_prod_mk_left ht _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
| Measurable fun a => ∫⁻ (b : β), indicator t (Function.const (α × β) c) (a, b) ∂↑κ a
[PROOFSTEP]
  congr
  ext
  erw [lintegral_indicator_const_comp measurable_prod_mk_left ht _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
| Measurable fun a => ∫⁻ (b : β), indicator t (Function.const (α × β) c) (a, b) ∂↑κ a
[PROOFSTEP]
congr
[GOAL]
case f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
| fun a => ∫⁻ (b : β), indicator t (Function.const (α × β) c) (a, b) ∂↑κ a
[PROOFSTEP]
ext
[GOAL]
case f.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
x✝ : α
| ∫⁻ (b : β), indicator t (Function.const (α × β) c) (x✝, b) ∂↑κ x✝
[PROOFSTEP]
erw [lintegral_indicator_const_comp measurable_prod_mk_left ht _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable fun x => c * ↑↑(↑κ x) (Prod.mk x ⁻¹' t)
[PROOFSTEP]
exact Measurable.const_mul (measurable_kernel_prod_mk_left ht) c
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
⊢ Measurable fun a => ∫⁻ (b : β), f a b ∂↑κ a
[PROOFSTEP]
let F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
⊢ Measurable fun a => ∫⁻ (b : β), f a b ∂↑κ a
[PROOFSTEP]
have h : ∀ a, ⨆ n, F n a = uncurry f a := SimpleFunc.iSup_eapprox_apply (uncurry f) hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α × β), ⨆ (n : ℕ), ↑(F n) a = uncurry f a
⊢ Measurable fun a => ∫⁻ (b : β), f a b ∂↑κ a
[PROOFSTEP]
simp only [Prod.forall, uncurry_apply_pair] at h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
⊢ Measurable fun a => ∫⁻ (b : β), f a b ∂↑κ a
[PROOFSTEP]
simp_rw [← h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
⊢ Measurable fun a => ∫⁻ (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) ∂↑κ a
[PROOFSTEP]
have : ∀ a, (∫⁻ b, ⨆ n, F n (a, b) ∂κ a) = ⨆ n, ∫⁻ b, F n (a, b) ∂κ a :=
  by
  intro a
  rw [lintegral_iSup]
  · exact fun n => (F n).measurable.comp measurable_prod_mk_left
  · exact fun i j hij b => SimpleFunc.monotone_eapprox (uncurry f) hij _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
⊢ ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
a : α
⊢ ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
[PROOFSTEP]
rw [lintegral_iSup]
[GOAL]
case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
a : α
⊢ ∀ (n : ℕ), Measurable fun b => ↑(F n) (a, b)
[PROOFSTEP]
exact fun n => (F n).measurable.comp measurable_prod_mk_left
[GOAL]
case h_mono
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝ : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
a : α
⊢ Monotone fun n b => ↑(F n) (a, b)
[PROOFSTEP]
exact fun i j hij b => SimpleFunc.monotone_eapprox (uncurry f) hij _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
⊢ Measurable fun a => ∫⁻ (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) ∂↑κ a
[PROOFSTEP]
simp_rw [this]
  -- Porting note: trouble finding the induction motive
    -- refine' measurable_iSup fun n => SimpleFunc.induction _ _ (F n)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
⊢ Measurable fun a => ⨆ (n : ℕ), ∫⁻ (b : β), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) ∂↑κ a
[PROOFSTEP]
refine' measurable_iSup fun n => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
n : ℕ
⊢ Measurable fun a => ∫⁻ (b : β), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) ∂↑κ a
[PROOFSTEP]
refine' SimpleFunc.induction (P := fun f => Measurable (fun (a : α) => ∫⁻ (b : β), f (a, b) ∂κ a)) _ _ (F n)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
n : ℕ
⊢ ∀ (c : ℝ≥0∞) {s : Set (α × β)} (hs : MeasurableSet s),
    (fun f => Measurable fun a => ∫⁻ (b : β), ↑f (a, b) ∂↑κ a)
      (SimpleFunc.piecewise s hs (SimpleFunc.const (α × β) c) (SimpleFunc.const (α × β) 0))
[PROOFSTEP]
intro c t ht
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
n : ℕ
c : ℝ≥0∞
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable fun a =>
    ∫⁻ (b : β), ↑(SimpleFunc.piecewise t ht (SimpleFunc.const (α × β) c) (SimpleFunc.const (α × β) 0)) (a, b) ∂↑κ a
[PROOFSTEP]
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const, SimpleFunc.coe_zero,
  Set.piecewise_eq_indicator]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
n : ℕ
c : ℝ≥0∞
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable fun a => ∫⁻ (b : β), Set.piecewise t (Function.const (α × β) c) 0 (a, b) ∂↑κ a
[PROOFSTEP]
exact kernel.measurable_lintegral_indicator_const (κ := κ) ht c
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
n : ℕ
⊢ ∀ ⦃f g : SimpleFunc (α × β) ℝ≥0∞⦄,
    Disjoint (support ↑f) (support ↑g) →
      (fun f => Measurable fun a => ∫⁻ (b : β), ↑f (a, b) ∂↑κ a) f →
        (fun f => Measurable fun a => ∫⁻ (b : β), ↑f (a, b) ∂↑κ a) g →
          (fun f => Measurable fun a => ∫⁻ (b : β), ↑f (a, b) ∂↑κ a) (f + g)
[PROOFSTEP]
intro g₁ g₂ _ hm₁ hm₂
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
a✝ : Disjoint (support ↑g₁) (support ↑g₂)
hm₁ : Measurable fun a => ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a
hm₂ : Measurable fun a => ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a
⊢ Measurable fun a => ∫⁻ (b : β), ↑(g₁ + g₂) (a, b) ∂↑κ a
[PROOFSTEP]
simp only [SimpleFunc.coe_add, Pi.add_apply]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
a✝ : Disjoint (support ↑g₁) (support ↑g₂)
hm₁ : Measurable fun a => ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a
hm₂ : Measurable fun a => ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a
⊢ Measurable fun a => ∫⁻ (b : β), ↑g₁ (a, b) + ↑g₂ (a, b) ∂↑κ a
[PROOFSTEP]
have h_add :
  (fun a => ∫⁻ b, g₁ (a, b) + g₂ (a, b) ∂κ a) = (fun a => ∫⁻ b, g₁ (a, b) ∂κ a) + fun a => ∫⁻ b, g₂ (a, b) ∂κ a :=
  by
  ext1 a
  rw [Pi.add_apply]
    -- Porting note: was `rw` (`Function.comp` reducibility)
  erw [lintegral_add_left (g₁.measurable.comp measurable_prod_mk_left)]
  simp_rw [Function.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
a✝ : Disjoint (support ↑g₁) (support ↑g₂)
hm₁ : Measurable fun a => ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a
hm₂ : Measurable fun a => ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a
⊢ (fun a => ∫⁻ (b : β), ↑g₁ (a, b) + ↑g₂ (a, b) ∂↑κ a) =
    (fun a => ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a) + fun a => ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a
[PROOFSTEP]
ext1 a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝¹ : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
a✝ : Disjoint (support ↑g₁) (support ↑g₂)
hm₁ : Measurable fun a => ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a
hm₂ : Measurable fun a => ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a
a : α
⊢ ∫⁻ (b : β), ↑g₁ (a, b) + ↑g₂ (a, b) ∂↑κ a =
    ((fun a => ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a) + fun a => ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a) a
[PROOFSTEP]
rw [Pi.add_apply]
  -- Porting note: was `rw` (`Function.comp` reducibility)
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝¹ : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
a✝ : Disjoint (support ↑g₁) (support ↑g₂)
hm₁ : Measurable fun a => ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a
hm₂ : Measurable fun a => ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a
a : α
⊢ ∫⁻ (b : β), ↑g₁ (a, b) + ↑g₂ (a, b) ∂↑κ a = ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a + ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a
[PROOFSTEP]
erw [lintegral_add_left (g₁.measurable.comp measurable_prod_mk_left)]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a✝¹ : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
a✝ : Disjoint (support ↑g₁) (support ↑g₂)
hm₁ : Measurable fun a => ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a
hm₂ : Measurable fun a => ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a
a : α
⊢ ∫⁻ (a_1 : β), (↑g₁ ∘ Prod.mk a) a_1 ∂↑κ a + ∫⁻ (a_1 : β), ↑g₂ (a, a_1) ∂↑κ a =
    ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a + ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a
[PROOFSTEP]
simp_rw [Function.comp_apply]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
a✝ : Disjoint (support ↑g₁) (support ↑g₂)
hm₁ : Measurable fun a => ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a
hm₂ : Measurable fun a => ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a
h_add :
  (fun a => ∫⁻ (b : β), ↑g₁ (a, b) + ↑g₂ (a, b) ∂↑κ a) =
    (fun a => ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a) + fun a => ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a
⊢ Measurable fun a => ∫⁻ (b : β), ↑g₁ (a, b) + ↑g₂ (a, b) ∂↑κ a
[PROOFSTEP]
rw [h_add]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), ↑(SimpleFunc.eapprox (uncurry f) n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ (n : ℕ), ↑(F n) (a, b) ∂↑κ a = ⨆ (n : ℕ), ∫⁻ (b : β), ↑(F n) (a, b) ∂↑κ a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
a✝ : Disjoint (support ↑g₁) (support ↑g₂)
hm₁ : Measurable fun a => ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a
hm₂ : Measurable fun a => ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a
h_add :
  (fun a => ∫⁻ (b : β), ↑g₁ (a, b) + ↑g₂ (a, b) ∂↑κ a) =
    (fun a => ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a) + fun a => ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a
⊢ Measurable ((fun a => ∫⁻ (b : β), ↑g₁ (a, b) ∂↑κ a) + fun a => ∫⁻ (b : β), ↑g₂ (a, b) ∂↑κ a)
[PROOFSTEP]
exact Measurable.add hm₁ hm₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a => ∫⁻ (b : β), f (a, b) ∂↑κ a
[PROOFSTEP]
refine' Measurable.lintegral_kernel_prod_right _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable (uncurry fun a b => f (a, b))
[PROOFSTEP]
have : (uncurry fun (a : α) (b : β) => f (a, b)) = f := by ext x; rw [← @Prod.mk.eta _ _ x, uncurry_apply_pair]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ (uncurry fun a b => f (a, b)) = f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α × β → ℝ≥0∞
hf : Measurable f
x : α × β
⊢ uncurry (fun a b => f (a, b)) x = f x
[PROOFSTEP]
rw [← @Prod.mk.eta _ _ x, uncurry_apply_pair]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α × β → ℝ≥0∞
hf : Measurable f
this : (uncurry fun a b => f (a, b)) = f
⊢ Measurable (uncurry fun a b => f (a, b))
[PROOFSTEP]
rwa [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : β × γ → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun x => ∫⁻ (y : γ), f (x, y) ∂↑η (a, x)
[PROOFSTEP]
change
  Measurable
    ((fun x => ∫⁻ y, (fun u : (α × β) × γ => f (u.1.2, u.2)) (x, y) ∂η x) ∘ Prod.mk a)
      -- Porting note: specified `κ`, `f`.
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : β × γ → ℝ≥0∞
hf : Measurable f
⊢ Measurable ((fun x => ∫⁻ (y : γ), (fun u => f (u.fst.snd, u.snd)) (x, y) ∂↑η x) ∘ Prod.mk a)
[PROOFSTEP]
refine'
  (Measurable.lintegral_kernel_prod_right' (κ := η) (f := (fun u ↦ f (u.fst.snd, u.snd))) _).comp
    measurable_prod_mk_left
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : β × γ → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun u => f (u.fst.snd, u.snd)
[PROOFSTEP]
exact hf.comp (measurable_fst.snd.prod_mk measurable_snd)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a => ∫⁻ (b : β) in s, f a b ∂↑κ a
[PROOFSTEP]
simp_rw [← lintegral_restrict κ hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a => ∫⁻ (b : β), f a b ∂↑(kernel.restrict κ hs) a
[PROOFSTEP]
exact hf.lintegral_kernel_prod_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : β → α → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ∫⁻ (a : β) in s, f a b ∂↑κ b
[PROOFSTEP]
simp_rw [← lintegral_restrict κ hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : β → α → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ∫⁻ (a : β), f a b ∂↑(kernel.restrict κ hs) b
[PROOFSTEP]
exact hf.lintegral_kernel_prod_left
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : β → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a => ∫⁻ (b : β) in s, f b ∂↑κ a
[PROOFSTEP]
refine Measurable.set_lintegral_kernel_prod_right ?_ hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : β → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable (uncurry fun a b => f b)
[PROOFSTEP]
convert (hf.comp measurable_snd)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet {x | Integrable (f x)}
[PROOFSTEP]
simp_rw [Integrable, hf.of_uncurry_left.aestronglyMeasurable, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet {x | HasFiniteIntegral (f x)}
[PROOFSTEP]
exact measurableSet_lt (Measurable.lintegral_kernel_prod_right hf.ennnorm) measurable_const
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂↑κ x
[PROOFSTEP]
classical
borelize E
haveI : TopologicalSpace.SeparableSpace (range (uncurry f) ∪ {0} : Set E) := hf.separableSpace_range_union_singleton
let s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn _ hf.measurable (range (uncurry f) ∪ {0}) 0 (by simp)
let s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) measurable_prod_mk_left
let f' : ℕ → α → E := fun n => {x | Integrable (f x) (κ x)}.indicator fun x => (s' n x).integral (κ x)
have hf' : ∀ n, StronglyMeasurable (f' n) := by
  intro n; refine' StronglyMeasurable.indicator _ (measurableSet_kernel_integrable hf)
  have : ∀ x, ((s' n x).range.filter fun x => x ≠ 0) ⊆ (s n).range :=
    by
    intro x; refine' Finset.Subset.trans (Finset.filter_subset _ _) _; intro y
    simp_rw [SimpleFunc.mem_range]; rintro ⟨z, rfl⟩; exact ⟨(x, z), rfl⟩
  simp only [SimpleFunc.integral_eq_sum_of_subset (this _)]
  refine' Finset.stronglyMeasurable_sum _ fun x _ => _
  refine' (Measurable.ennreal_toReal _).stronglyMeasurable.smul_const _
  simp (config := { singlePass := true }) only [SimpleFunc.coe_comp, preimage_comp]
  apply kernel.measurable_kernel_prod_mk_left
  exact (s n).measurableSet_fiber x
have h2f' : Tendsto f' atTop (𝓝 fun x : α => ∫ y : β, f x y ∂κ x) :=
  by
  rw [tendsto_pi_nhds]; intro x
  by_cases hfx : Integrable (f x) (κ x)
  · have : ∀ n, Integrable (s' n x) (κ x) := by
      intro n; apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
      apply eventually_of_forall; intro y
      simp_rw [SimpleFunc.coe_comp]; exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
    simp only [hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem, mem_setOf_eq]
    refine'
      tendsto_integral_of_dominated_convergence (fun y => ‖f x y‖ + ‖f x y‖) (fun n => (s' n x).aestronglyMeasurable)
        (hfx.norm.add hfx.norm) _ _
    ·
      -- Porting note: was
              -- exact fun n => eventually_of_forall fun y =>
              --   SimpleFunc.norm_approxOn_zero_le _ _ (x, y) nexact fun n =>
        eventually_of_forall fun y => SimpleFunc.norm_approxOn_zero_le hf.measurable (by simp) (x, y) n
    ·
      -- Porting note:
              -- refine' eventually_of_forall fun y => SimpleFunc.tendsto_approxOn _ _ _
      refine' eventually_of_forall fun y => SimpleFunc.tendsto_approxOn hf.measurable (by simp) _
      apply subset_closure
      simp [-uncurry_apply_pair]
  · simp [hfx, integral_undef]
exact stronglyMeasurable_of_tendsto _ hf' h2f'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂↑κ x
[PROOFSTEP]
borelize E
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂↑κ x
[PROOFSTEP]
haveI : TopologicalSpace.SeparableSpace (range (uncurry f) ∪ {0} : Set E) := hf.separableSpace_range_union_singleton
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂↑κ x
[PROOFSTEP]
let s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn _ hf.measurable (range (uncurry f) ∪ {0}) 0 (by simp)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
⊢ 0 ∈ range (uncurry f) ∪ {0}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂↑κ x
[PROOFSTEP]
let s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) measurable_prod_mk_left
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂↑κ x
[PROOFSTEP]
let f' : ℕ → α → E := fun n => {x | Integrable (f x) (κ x)}.indicator fun x => (s' n x).integral (κ x)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂↑κ x
[PROOFSTEP]
have hf' : ∀ n, StronglyMeasurable (f' n) := by
  intro n; refine' StronglyMeasurable.indicator _ (measurableSet_kernel_integrable hf)
  have : ∀ x, ((s' n x).range.filter fun x => x ≠ 0) ⊆ (s n).range :=
    by
    intro x; refine' Finset.Subset.trans (Finset.filter_subset _ _) _; intro y
    simp_rw [SimpleFunc.mem_range]; rintro ⟨z, rfl⟩; exact ⟨(x, z), rfl⟩
  simp only [SimpleFunc.integral_eq_sum_of_subset (this _)]
  refine' Finset.stronglyMeasurable_sum _ fun x _ => _
  refine' (Measurable.ennreal_toReal _).stronglyMeasurable.smul_const _
  simp (config := { singlePass := true }) only [SimpleFunc.coe_comp, preimage_comp]
  apply kernel.measurable_kernel_prod_mk_left
  exact (s n).measurableSet_fiber x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
⊢ ∀ (n : ℕ), StronglyMeasurable (f' n)
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
⊢ StronglyMeasurable (f' n)
[PROOFSTEP]
refine' StronglyMeasurable.indicator _ (measurableSet_kernel_integrable hf)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
⊢ StronglyMeasurable fun x => SimpleFunc.integral (↑κ x) (s' n x)
[PROOFSTEP]
have : ∀ x, ((s' n x).range.filter fun x => x ≠ 0) ⊆ (s n).range :=
  by
  intro x; refine' Finset.Subset.trans (Finset.filter_subset _ _) _; intro y
  simp_rw [SimpleFunc.mem_range]; rintro ⟨z, rfl⟩; exact ⟨(x, z), rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
⊢ ∀ (x : α), Finset.filter (fun x => x ≠ 0) (SimpleFunc.range (s' n x)) ⊆ SimpleFunc.range (s n)
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
x : α
⊢ Finset.filter (fun x => x ≠ 0) (SimpleFunc.range (s' n x)) ⊆ SimpleFunc.range (s n)
[PROOFSTEP]
refine' Finset.Subset.trans (Finset.filter_subset _ _) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
x : α
⊢ SimpleFunc.range (s' n x) ⊆ SimpleFunc.range (s n)
[PROOFSTEP]
intro y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
x : α
y : E
⊢ y ∈ SimpleFunc.range (s' n x) → y ∈ SimpleFunc.range (s n)
[PROOFSTEP]
simp_rw [SimpleFunc.mem_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
x : α
y : E
⊢ y ∈
      range
        ↑(SimpleFunc.comp
            (SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
              (_ : 0 ∈ range (uncurry f) ∪ {0}) n)
            (Prod.mk x) (_ : Measurable (Prod.mk x))) →
    y ∈
      range
        ↑(SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
            (_ : 0 ∈ range (uncurry f) ∪ {0}) n)
[PROOFSTEP]
rintro ⟨z, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
x : α
z : β
⊢ ↑(SimpleFunc.comp
          (SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
            (_ : 0 ∈ range (uncurry f) ∪ {0}) n)
          (Prod.mk x) (_ : Measurable (Prod.mk x)))
      z ∈
    range
      ↑(SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
          (_ : 0 ∈ range (uncurry f) ∪ {0}) n)
[PROOFSTEP]
exact ⟨(x, z), rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
this : ∀ (x : α), Finset.filter (fun x => x ≠ 0) (SimpleFunc.range (s' n x)) ⊆ SimpleFunc.range (s n)
⊢ StronglyMeasurable fun x => SimpleFunc.integral (↑κ x) (s' n x)
[PROOFSTEP]
simp only [SimpleFunc.integral_eq_sum_of_subset (this _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
this : ∀ (x : α), Finset.filter (fun x => x ≠ 0) (SimpleFunc.range (s' n x)) ⊆ SimpleFunc.range (s n)
⊢ StronglyMeasurable fun x =>
    Finset.sum
      (SimpleFunc.range
        (SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
          (_ : 0 ∈ range (uncurry f) ∪ {0}) n))
      fun x_1 =>
      ENNReal.toReal
          (↑↑(↑κ x)
            (↑(SimpleFunc.comp
                  (SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
                    (_ : 0 ∈ range (uncurry f) ∪ {0}) n)
                  (Prod.mk x) (_ : Measurable (Prod.mk x))) ⁻¹'
              {x_1})) •
        x_1
[PROOFSTEP]
refine' Finset.stronglyMeasurable_sum _ fun x _ => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
this : ∀ (x : α), Finset.filter (fun x => x ≠ 0) (SimpleFunc.range (s' n x)) ⊆ SimpleFunc.range (s n)
x : E
x✝ :
  x ∈
    SimpleFunc.range
      (SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
        (_ : 0 ∈ range (uncurry f) ∪ {0}) n)
⊢ StronglyMeasurable fun x_1 =>
    ENNReal.toReal
        (↑↑(↑κ x_1)
          (↑(SimpleFunc.comp
                (SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
                  (_ : 0 ∈ range (uncurry f) ∪ {0}) n)
                (Prod.mk x_1) (_ : Measurable (Prod.mk x_1))) ⁻¹'
            {x})) •
      x
[PROOFSTEP]
refine' (Measurable.ennreal_toReal _).stronglyMeasurable.smul_const _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
this : ∀ (x : α), Finset.filter (fun x => x ≠ 0) (SimpleFunc.range (s' n x)) ⊆ SimpleFunc.range (s n)
x : E
x✝ :
  x ∈
    SimpleFunc.range
      (SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
        (_ : 0 ∈ range (uncurry f) ∪ {0}) n)
⊢ Measurable fun x_1 =>
    ↑↑(↑κ x_1)
      (↑(SimpleFunc.comp
            (SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
              (_ : 0 ∈ range (uncurry f) ∪ {0}) n)
            (Prod.mk x_1) (_ : Measurable (Prod.mk x_1))) ⁻¹'
        {x})
[PROOFSTEP]
simp (config := { singlePass := true }) only [SimpleFunc.coe_comp, preimage_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
this : ∀ (x : α), Finset.filter (fun x => x ≠ 0) (SimpleFunc.range (s' n x)) ⊆ SimpleFunc.range (s n)
x : E
x✝ :
  x ∈
    SimpleFunc.range
      (SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
        (_ : 0 ∈ range (uncurry f) ∪ {0}) n)
⊢ Measurable fun x_1 =>
    ↑↑(↑κ x_1)
      (Prod.mk x_1 ⁻¹'
        (↑(SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
              (_ : 0 ∈ range (uncurry f) ∪ {0}) n) ⁻¹'
          {x}))
[PROOFSTEP]
apply kernel.measurable_kernel_prod_mk_left
[GOAL]
case ht
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
n : ℕ
this : ∀ (x : α), Finset.filter (fun x => x ≠ 0) (SimpleFunc.range (s' n x)) ⊆ SimpleFunc.range (s n)
x : E
x✝ :
  x ∈
    SimpleFunc.range
      (SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
        (_ : 0 ∈ range (uncurry f) ∪ {0}) n)
⊢ MeasurableSet
    (↑(SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
          (_ : 0 ∈ range (uncurry f) ∪ {0}) n) ⁻¹'
      {x})
[PROOFSTEP]
exact (s n).measurableSet_fiber x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂↑κ x
[PROOFSTEP]
have h2f' : Tendsto f' atTop (𝓝 fun x : α => ∫ y : β, f x y ∂κ x) :=
  by
  rw [tendsto_pi_nhds]; intro x
  by_cases hfx : Integrable (f x) (κ x)
  · have : ∀ n, Integrable (s' n x) (κ x) := by
      intro n; apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
      apply eventually_of_forall; intro y
      simp_rw [SimpleFunc.coe_comp]; exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
    simp only [hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem, mem_setOf_eq]
    refine'
      tendsto_integral_of_dominated_convergence (fun y => ‖f x y‖ + ‖f x y‖) (fun n => (s' n x).aestronglyMeasurable)
        (hfx.norm.add hfx.norm) _ _
    ·
      -- Porting note: was
              -- exact fun n => eventually_of_forall fun y =>
              --   SimpleFunc.norm_approxOn_zero_le _ _ (x, y) nexact fun n =>
        eventually_of_forall fun y => SimpleFunc.norm_approxOn_zero_le hf.measurable (by simp) (x, y) n
    ·
      -- Porting note:
              -- refine' eventually_of_forall fun y => SimpleFunc.tendsto_approxOn _ _ _
      refine' eventually_of_forall fun y => SimpleFunc.tendsto_approxOn hf.measurable (by simp) _
      apply subset_closure
      simp [-uncurry_apply_pair]
  · simp [hfx, integral_undef]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
⊢ Tendsto f' atTop (𝓝 fun x => ∫ (y : β), f x y ∂↑κ x)
[PROOFSTEP]
rw [tendsto_pi_nhds]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
⊢ ∀ (x : α), Tendsto (fun i => f' i x) atTop (𝓝 (∫ (y : β), f x y ∂↑κ x))
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
⊢ Tendsto (fun i => f' i x) atTop (𝓝 (∫ (y : β), f x y ∂↑κ x))
[PROOFSTEP]
by_cases hfx : Integrable (f x) (κ x)
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
⊢ Tendsto (fun i => f' i x) atTop (𝓝 (∫ (y : β), f x y ∂↑κ x))
[PROOFSTEP]
have : ∀ n, Integrable (s' n x) (κ x) := by
  intro n; apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
  apply eventually_of_forall; intro y
  simp_rw [SimpleFunc.coe_comp]; exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
⊢ ∀ (n : ℕ), Integrable ↑(s' n x)
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
n : ℕ
⊢ Integrable ↑(s' n x)
[PROOFSTEP]
apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
n : ℕ
⊢ ∀ᵐ (a : β) ∂↑κ x, ‖↑(s' n x) a‖ ≤ ((fun a => ‖f x a‖) + fun a => ‖f x a‖) a
[PROOFSTEP]
apply eventually_of_forall
[GOAL]
case hp
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
n : ℕ
⊢ ∀ (x_1 : β), ‖↑(s' n x) x_1‖ ≤ ((fun a => ‖f x a‖) + fun a => ‖f x a‖) x_1
[PROOFSTEP]
intro y
[GOAL]
case hp
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
n : ℕ
y : β
⊢ ‖↑(s' n x) y‖ ≤ ((fun a => ‖f x a‖) + fun a => ‖f x a‖) y
[PROOFSTEP]
simp_rw [SimpleFunc.coe_comp]
[GOAL]
case hp
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
n : ℕ
y : β
⊢ ‖(↑(SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
              (_ : 0 ∈ range (uncurry f) ∪ {0}) n) ∘
          Prod.mk x)
        y‖ ≤
    ((fun a => ‖f x a‖) + fun a => ‖f x a‖) y
[PROOFSTEP]
exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
this : ∀ (n : ℕ), Integrable ↑(s' n x)
⊢ Tendsto (fun i => f' i x) atTop (𝓝 (∫ (y : β), f x y ∂↑κ x))
[PROOFSTEP]
simp only [hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem, mem_setOf_eq]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
this : ∀ (n : ℕ), Integrable ↑(s' n x)
⊢ Tendsto
    (fun i =>
      ∫ (x_1 : β),
        ↑(SimpleFunc.comp
              (SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
                (_ : 0 ∈ range (uncurry f) ∪ {0}) i)
              (Prod.mk x) (_ : Measurable (Prod.mk x)))
          x_1 ∂↑κ x)
    atTop (𝓝 (∫ (y : β), f x y ∂↑κ x))
[PROOFSTEP]
refine'
  tendsto_integral_of_dominated_convergence (fun y => ‖f x y‖ + ‖f x y‖) (fun n => (s' n x).aestronglyMeasurable)
    (hfx.norm.add hfx.norm) _ _
[GOAL]
case pos.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
this : ∀ (n : ℕ), Integrable ↑(s' n x)
⊢ ∀ (n : ℕ),
    ∀ᵐ (a : β) ∂↑κ x,
      ‖↑(SimpleFunc.comp
                (SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
                  (_ : 0 ∈ range (uncurry f) ∪ {0}) n)
                (Prod.mk x) (_ : Measurable (Prod.mk x)))
            a‖ ≤
        (fun y => ‖f x y‖ + ‖f x y‖) a
[PROOFSTEP]
exact fun n => eventually_of_forall fun y => SimpleFunc.norm_approxOn_zero_le hf.measurable (by simp) (x, y) n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
this : ∀ (n : ℕ), Integrable ↑(s' n x)
n : ℕ
y : β
⊢ 0 ∈ range (uncurry f) ∪ {0}
[PROOFSTEP]
simp
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
this : ∀ (n : ℕ), Integrable ↑(s' n x)
⊢ ∀ᵐ (a : β) ∂↑κ x,
    Tendsto
      (fun n =>
        ↑(SimpleFunc.comp
              (SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
                (_ : 0 ∈ range (uncurry f) ∪ {0}) n)
              (Prod.mk x) (_ : Measurable (Prod.mk x)))
          a)
      atTop (𝓝 (f x a))
[PROOFSTEP]
refine' eventually_of_forall fun y => SimpleFunc.tendsto_approxOn hf.measurable (by simp) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
this : ∀ (n : ℕ), Integrable ↑(s' n x)
y : β
⊢ 0 ∈ range (uncurry f) ∪ {0}
[PROOFSTEP]
simp
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
this : ∀ (n : ℕ), Integrable ↑(s' n x)
y : β
⊢ uncurry f (x, y) ∈ closure (range (uncurry f) ∪ {0})
[PROOFSTEP]
apply subset_closure
[GOAL]
case pos.refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x)
this : ∀ (n : ℕ), Integrable ↑(s' n x)
y : β
⊢ uncurry f (x, y) ∈ range (uncurry f) ∪ {0}
[PROOFSTEP]
simp [-uncurry_apply_pair]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : ¬Integrable (f x)
⊢ Tendsto (fun i => f' i x) atTop (𝓝 (∫ (y : β), f x y ∂↑κ x))
[PROOFSTEP]
simp [hfx, integral_undef]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → E
hf : StronglyMeasurable (uncurry f)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E :=
  SimpleFunc.approxOn (uncurry f) (_ : Measurable (uncurry f)) (range (uncurry f) ∪ {0}) 0
    (_ : 0 ∈ range (uncurry f) ∪ {0})
s' : ℕ → α → SimpleFunc β E := fun n x => SimpleFunc.comp (s n) (Prod.mk x) (_ : Measurable (Prod.mk x))
f' : ℕ → α → E := fun n => indicator {x | Integrable (f x)} fun x => SimpleFunc.integral (↑κ x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
h2f' : Tendsto f' atTop (𝓝 fun x => ∫ (y : β), f x y ∂↑κ x)
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂↑κ x
[PROOFSTEP]
exact stronglyMeasurable_of_tendsto _ hf' h2f'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂↑κ x
[PROOFSTEP]
rw [← uncurry_curry f] at hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α × β → E
hf : StronglyMeasurable (uncurry (curry f))
⊢ StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂↑κ x
[PROOFSTEP]
exact hf.integral_kernel_prod_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : β × γ → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun x => ∫ (y : γ), f (x, y) ∂↑η (a, x)
[PROOFSTEP]
change StronglyMeasurable ((fun x => ∫ y, (fun u : (α × β) × γ => f (u.1.2, u.2)) (x, y) ∂η x) ∘ fun x => (a, x))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : β × γ → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable ((fun x => ∫ (y : γ), (fun u => f (u.fst.snd, u.snd)) (x, y) ∂↑η x) ∘ fun x => (a, x))
[PROOFSTEP]
refine' StronglyMeasurable.comp_measurable _ measurable_prod_mk_left
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : β × γ → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun x => ∫ (y : γ), (fun u => f (u.fst.snd, u.snd)) (x, y) ∂↑η x
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : β × γ → E
hf : StronglyMeasurable f
⊢ MeasurableSpace α
[PROOFSTEP]
have :=
  MeasureTheory.StronglyMeasurable.integral_kernel_prod_right' (κ := η)
    (hf.comp_measurable (measurable_fst.snd.prod_mk measurable_snd))
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : β × γ → E
hf : StronglyMeasurable f
this : StronglyMeasurable fun x => ∫ (y : γ), (f ∘ fun a => (a.fst.snd, a.snd)) (x, y) ∂↑η x
⊢ StronglyMeasurable fun x => ∫ (y : γ), (fun u => f (u.fst.snd, u.snd)) (x, y) ∂↑η x
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : β × γ → E
hf : StronglyMeasurable f
⊢ MeasurableSpace α
[PROOFSTEP]
simpa using this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : γ × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun y => ∫ (x : γ), f (x, y) ∂↑η (a, y)
[PROOFSTEP]
change StronglyMeasurable ((fun y => ∫ x, (fun u : γ × α × β => f (u.1, u.2.2)) (x, y) ∂η y) ∘ fun x => (a, x))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : γ × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable ((fun y => ∫ (x : γ), (fun u => f (u.fst, u.snd.snd)) (x, y) ∂↑η y) ∘ fun x => (a, x))
[PROOFSTEP]
refine' StronglyMeasurable.comp_measurable _ measurable_prod_mk_left
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : γ × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun y => ∫ (x : γ), (fun u => f (u.fst, u.snd.snd)) (x, y) ∂↑η y
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : γ × β → E
hf : StronglyMeasurable f
⊢ MeasurableSpace α
[PROOFSTEP]
have :=
  MeasureTheory.StronglyMeasurable.integral_kernel_prod_left' (κ := η)
    (hf.comp_measurable (measurable_fst.prod_mk measurable_snd.snd))
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : γ × β → E
hf : StronglyMeasurable f
this : StronglyMeasurable fun y => ∫ (x : γ), (f ∘ fun a => (a.fst, a.snd.snd)) (x, y) ∂↑η y
⊢ StronglyMeasurable fun y => ∫ (x : γ), (fun u => f (u.fst, u.snd.snd)) (x, y) ∂↑η y
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
η : { x // x ∈ kernel (α × β) γ }
a : α
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : γ × β → E
hf : StronglyMeasurable f
⊢ MeasurableSpace α
[PROOFSTEP]
simpa using this