-- Mathlib/Probability/Kernel/MeasurableIntegral.lean
theorem StronglyMeasurable.integral_kernel ⦃f : β → E⦄
    (hf : StronglyMeasurable f) : StronglyMeasurable fun x ↦ ∫ y, f y ∂κ x

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ StronglyMeasurable fun x => ∫ (y : β), f y ∂κ x

Tactic:
have : TopologicalSpace.SeparableSpace (range f ∪ {0} : Set E) :=
  hf.separableSpace_range_union_singleton

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
⊢ StronglyMeasurable fun x => ∫ (y : β), f y ∂κ x

Proof state:
case pos.refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n => {x | Integrable f (κ x)}.indicator fun x => SimpleFunc.integral (κ x) (s n)
n : ℕ
x✝¹ : E
x✝ : x✝¹ ∈ (s n).range
⊢ Measurable fun x => (κ x) (⇑(s n) ⁻¹' {x✝¹})

Tactic:
exact κ.measurable_coe ((s n).measurableSet_fiber _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
⊢ 0 ∈ range f ∪ {0}

Tactic:
simp

Result:
no goals

Proof state:
case pos.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n => {x | Integrable f (κ x)}.indicator fun x => SimpleFunc.integral (κ x) (s n)
⊢ Tendsto f' atTop (𝓝 fun x => ∫ (y : β), f y ∂κ x)

Tactic:
rw [tendsto_pi_nhds]

Result:
case pos.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n => {x | Integrable f (κ x)}.indicator fun x => SimpleFunc.integral (κ x) (s n)
⊢ ∀ (x : α), Tendsto (fun i => f' i x) atTop (𝓝 (∫ (y : β), f y ∂κ x))

Proof state:
case pos.refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n => {x | Integrable f (κ x)}.indicator fun x => SimpleFunc.integral (κ x) (s n)
n : ℕ
⊢ StronglyMeasurable fun x => SimpleFunc.integral (κ x) (s n)

Tactic:
simp_rw [SimpleFunc.integral_eq]

Result:
case pos.refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n => {x | Integrable f (κ x)}.indicator fun x => SimpleFunc.integral (κ x) (s n)
n : ℕ
⊢ StronglyMeasurable fun x => ∑ x_1 ∈ (s n).range, ((κ x) (⇑(s n) ⁻¹' {x_1})).toReal • x_1

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n => {x | Integrable f (κ x)}.indicator fun x => SimpleFunc.integral (κ x) (s n)
x : α
hfx : Integrable f (κ x)
⊢ Tendsto (fun i => f' i x) atTop (𝓝 (∫ (y : β), f y ∂κ x))

Tactic:
simp only [mem_setOf_eq, hfx, indicator_of_mem, f']

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n => {x | Integrable f (κ x)}.indicator fun x => SimpleFunc.integral (κ x) (s n)
x : α
hfx : Integrable f (κ x)
⊢ Tendsto (fun i => SimpleFunc.integral (κ x) (s i)) atTop (𝓝 (∫ (y : β), f y ∂κ x))

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
⊢ StronglyMeasurable fun x => ∫ (y : β), f y ∂κ x

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : ¬CompleteSpace E
⊢ StronglyMeasurable fun x => ∫ (y : β), f y ∂κ x

Tactic:
swap

Result:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : ¬CompleteSpace E
⊢ StronglyMeasurable fun x => ∫ (y : β), f y ∂κ x

case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
⊢ StronglyMeasurable fun x => ∫ (y : β), f y ∂κ x

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n => {x | Integrable f (κ x)}.indicator fun x => SimpleFunc.integral (κ x) (s n)
x : α
hfx : ¬Integrable f (κ x)
⊢ Tendsto (fun i => f' i x) atTop (𝓝 (∫ (y : β), f y ∂κ x))

Tactic:
simp [f', hfx, integral_undef]

Result:
no goals