awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
f : β → E
hf : StronglyMeasurable f
⊢ MeasurableSet.{u_1} (α := α) {a : α | @HasFiniteIntegral _ _ _ mβ f ((κ : (a : α) → Measure β) a)}

Tactic:
exact measurableSet_lt hf.enorm.lintegral_kernel measurable_const

Premises used: MeasureTheory.StronglyMeasurable.enorm, Measurable.lintegral_kernel, measurableSet_lt, measurable_const
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
f : α → β → E
hf : StronglyMeasurable (uncurry f)
simp_rw : MeasurableSet.{u_1} (α := α) {x : α | @HasFiniteIntegral _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)}
⊢ MeasurableSet.{u_1} (α := α) {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)}

Tactic:
simp_rw [Integrable, hf.of_uncurry_left.aestronglyMeasurable, true_and]

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Integrable, true_and, MeasureTheory.StronglyMeasurable.of_uncurry_left
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet.{u_1} (α := α) {x : α | @HasFiniteIntegral _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)}

Tactic:
measurableSet_lt (Measurable.lintegral_kernel_prod_right hf.enorm) measurable_const

Premises used: MeasureTheory.StronglyMeasurable.enorm, setOf, Measurable.lintegral_kernel_prod_right, measurableSet_lt, measurable_const, MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet.{u_1} (α := α) {x : α | @HasFiniteIntegral _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)}

Tactic:
exact measurableSet_lt (Measurable.lintegral_kernel_prod_right hf.enorm) measurable_const

Premises used: Measurable.lintegral_kernel_prod_right, measurableSet_lt, measurable_const
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
pos :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
neg :
  ∀ (hE : ¬CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : ¬CompleteSpace E
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y

Tactic:
simp [integral, hE, stronglyMeasurable_const]

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.integral
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)

Tactic:
have : TopologicalSpace.SeparableSpace (range f ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
⊢ 0 ∈ range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y

Tactic:
stronglyMeasurable_of_tendsto (f := f') atTop (fun n ↦ ?_) ?_

Premises used: stronglyMeasurable_of_tendsto, Filter.atTop
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
pos : ∀ (n : ℕ), StronglyMeasurable (f' n)
pos₁ : Tendsto f' atTop (𝓝 fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y)
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y

Tactic:
refine stronglyMeasurable_of_tendsto (f := f') atTop (fun n ↦ ?_) ?_

Premises used: stronglyMeasurable_of_tendsto, Filter.atTop
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
n : ℕ
⊢ StronglyMeasurable (f' n)

Tactic:
StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)

Premises used: ProbabilityTheory.measurableSet_integrable, MeasureTheory.StronglyMeasurable.indicator
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
n : ℕ
pos : StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦ SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
⊢ StronglyMeasurable (f' n)

Tactic:
refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)

Premises used: ProbabilityTheory.measurableSet_integrable, MeasureTheory.StronglyMeasurable.indicator
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
n : ℕ
pos :
  StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    ∑ x_1 ∈ (s n).range,
      Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x)
          (preimage (β := E) (⇑(s n) : (a : β) → E) {x_1}) •
        x_1
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦ SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)

Tactic:
simp_rw [SimpleFunc.integral_eq]

Premises used: MeasureTheory.SimpleFunc.integral_eq
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
n : ℕ
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    ∑ x_1 ∈ (s n).range,
      Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x)
          (preimage (β := E) (⇑(s n) : (a : β) → E) {x_1}) •
        x_1

Tactic:
Finset.stronglyMeasurable_fun_sum _ fun _ _ ↦ ?_

Premises used: Finset.stronglyMeasurable_fun_sum
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
n : ℕ
pos :
  ∀ x ∈ (s n).range,
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x_2 : α) ↦
      Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x_2)
          (preimage (β := E) (⇑(s n) : (a : β) → E) {x}) •
        x
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    ∑ x_1 ∈ (s n).range,
      Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x)
          (preimage (β := E) (⇑(s n) : (a : β) → E) {x_1}) •
        x_1

Tactic:
refine Finset.stronglyMeasurable_fun_sum _ fun _ _ ↦ ?_

Premises used: Finset.stronglyMeasurable_fun_sum
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
n : ℕ
x : E
h : x ∈ (s n).range
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x_1 : α) ↦
    Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x_1)
        (preimage (β := E) (⇑(s n) : (a : β) → E) {x}) •
      x

Tactic:
(Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _

Premises used: Measurable.stronglyMeasurable, MeasureTheory.Measure.real, MeasureTheory.StronglyMeasurable.smul_const, Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
n : ℕ
x : E
h : x ∈ (s n).range
pos :
  Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
    (((κ : (a : α) → Measure β) x_1 : Measure β) : (a : Set β) → ℝ≥0∞) (preimage (β := E) (⇑(s n) : (a : β) → E) {x})
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x_1 : α) ↦
    Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x_1)
        (preimage (β := E) (⇑(s n) : (a : β) → E) {x}) •
      x

Tactic:
refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _

Premises used: Measurable.stronglyMeasurable, MeasureTheory.StronglyMeasurable.smul_const, Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
n : ℕ
x : E
h : x ∈ (s n).range
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
    (((κ : (a : α) → Measure β) x_1 : Measure β) : (a : Set β) → ℝ≥0∞) (preimage (β := E) (⇑(s n) : (a : β) → E) {x})

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

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
n : ℕ
x : E
h : x ∈ (s n).range
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
    (((κ : (a : α) → Measure β) x_1 : Measure β) : (a : Set β) → ℝ≥0∞) (preimage (β := E) (⇑(s n) : (a : β) → E) {x})

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

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
pos :
  ∀ (x : α),
    Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
      (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))
⊢ Tendsto f' atTop (𝓝 fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y)

Tactic:
rw [tendsto_pi_nhds]

Premises used: tendsto_pi_nhds
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
x : α
pos :
  ∀ (hfx : @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)),
    Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
      (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))
neg :
  ∀ (hfx : ¬@Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)),
    Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
      (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))

Tactic:
by_cases hfx : Integrable f (κ x)

Premises used: MeasureTheory.Integrable, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
x : α
hfx : @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)
pos :
  Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s i)) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))

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

Premises used: Set.mem_setOf_eq, Set.indicator_of_mem
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
x : α
hfx : @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)
pos : range f ∪ {0} ⊆ range f ∪ {0}
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s i)) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))

Tactic:
apply tendsto_integral_approxOn_of_measurable_of_range_subset _ hfx

Premises used: MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
x : α
hfx : @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)
⊢ range f ∪ {0} ⊆ range f ∪ {0}

Tactic:
subset_rfl

Premises used: subset_rfl
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
x : α
hfx : @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)
⊢ range f ∪ {0} ⊆ range f ∪ {0}

Tactic:
exact subset_rfl

Premises used: subset_rfl
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
x : α
hfx : ¬@Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))

Tactic:
simp [f', hfx, integral_undef]

Premises used: MeasureTheory.integral_undef