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
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
pos :
  ∀ (hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)),
    Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
      (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
neg :
  ∀ (hfx : ¬@Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)),
    Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
      (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))

Tactic:
by_cases hfx : Integrable (f x) (κ 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 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
n : ℕ
apply :
  ∀ᵐ (a : β) ∂((κ : (a : α) → Measure β) x : Measure β),
    norm.{u_4} (E := E) ((s' n x : (a : β) → E) a : E) ≤
      HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) a
⊢ @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)

Tactic:
apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable

Premises used: MeasureTheory.Integrable.mono', MeasureTheory.Integrable.add, MeasureTheory.SimpleFunc.aestronglyMeasurable, MeasureTheory.Integrable.norm
-- 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 κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
n : ℕ
h :
  ∀ (y : β),
    norm.{u_4} (E := E) ((s' n x : (a : β) → E) y : E) ≤
      HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y
⊢ ∀ᵐ (a : β) ∂((κ : (a : α) → Measure β) x : Measure β),
    norm.{u_4} (E := E) ((s' n x : (a : β) → E) a : E) ≤
      HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) a

Tactic:
filter_upwards with y
-- 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 κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
n : ℕ
y : β
h :
  norm.{u_4} (E := E) (((⇑(s n) : (a : α × β) → E) ∘ Prod.mk x) y) ≤
    HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y
⊢ norm.{u_4} (E := E) ((s' n x : (a : β) → E) y : E) ≤
    HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y

Tactic:
simp_rw [s', SimpleFunc.coe_comp]

Premises used: MeasureTheory.SimpleFunc.coe_comp
-- 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 κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
n : ℕ
y : β
⊢ norm.{u_4} (E := E) (((⇑(s n) : (a : α × β) → E) ∘ Prod.mk x) y) ≤
    HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y

Tactic:
SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n

Premises used: Prod.mk, MeasureTheory.SimpleFunc.norm_approxOn_zero_le
-- 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 κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
n : ℕ
y : β
⊢ norm.{u_4} (E := E) (((⇑(s n) : (a : α × β) → E) ∘ Prod.mk x) y) ≤
    HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y

Tactic:
exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n

Premises used: Prod.mk, MeasureTheory.SimpleFunc.norm_approxOn_zero_le
-- 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 κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
⊢ ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)

Tactic:
have (n : _) : Integrable (s' n x) (κ x) := by
        apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
        filter_upwards with y
        simp_rw [s', SimpleFunc.coe_comp]; exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
-- 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 κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
pos :
  Tendsto.{0, u_4} (β := E)
    (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (x_1 : β) ↦ (s' i x : (a : β) → E) x_1) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))

Tactic:
simp only [f', hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem,
        mem_setOf_eq]

Premises used: MeasureTheory.SimpleFunc.integral_eq_integral, 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 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
⊢ Tendsto.{0, u_4} (β := E)
    (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (x_1 : β) ↦ (s' i x : (a : β) → E) x_1) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))

Tactic:
tendsto_integral_of_dominated_convergence (fun y => ‖f x y‖ + ‖f x y‖)
          (fun n => (s' n x).aestronglyMeasurable) (hfx.norm.add hfx.norm) ?_ ?_

Premises used: Norm.norm, MeasureTheory.tendsto_integral_of_dominated_convergence, HAdd.hAdd, MeasureTheory.Integrable.add, MeasureTheory.SimpleFunc.aestronglyMeasurable, MeasureTheory.Integrable.norm
-- 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 κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
pos :
  ∀ (n : ℕ),
    ∀ᵐ (a : β) ∂((κ : (a : α) → Measure β) x : Measure β),
      norm.{u_4} (E := E) ((s' n x : (a : β) → E) a : E) ≤ (fun (y : β) ↦ ‖f x y‖ + ‖f x y‖) a
pos₁ :
  ∀ᵐ (a : β) ∂((κ : (a : α) → Measure β) x : Measure β),
    Tendsto (fun (n : ℕ) ↦ (s' n x : (a : β) → E) a) atTop (𝓝 (f x a))
⊢ Tendsto.{0, u_4} (β := E)
    (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (x_1 : β) ↦ (s' i x : (a : β) → E) x_1) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))

Tactic:
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) ?_ ?_

Premises used: Norm.norm, MeasureTheory.tendsto_integral_of_dominated_convergence, HAdd.hAdd, MeasureTheory.Integrable.add, MeasureTheory.SimpleFunc.aestronglyMeasurable, MeasureTheory.Integrable.norm
-- 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 κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
n : ℕ
y : β
⊢ 0 ∈ range (uncurry 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 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
⊢ ∀ (n : ℕ),
    ∀ᵐ (a : β) ∂((κ : (a : α) → Measure β) x : Measure β),
      norm.{u_4} (E := E) ((s' n x : (a : β) → E) a : E) ≤ (fun (y : β) ↦ ‖f x y‖ + ‖f x y‖) a

Tactic:
exact fun n => Eventually.of_forall fun y =>
          SimpleFunc.norm_approxOn_zero_le hf.measurable (by simp) (x, y) n

Premises used: MeasureTheory.StronglyMeasurable.measurable, Prod.mk, Filter.Eventually.of_forall, MeasureTheory.SimpleFunc.norm_approxOn_zero_le
-- 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 κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
y : β
⊢ 0 ∈ range (uncurry 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 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
pos :
  ∀ (y : β), uncurry f (x, y) ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range (uncurry f) ∪ {0})
⊢ ∀ᵐ (a : β) ∂((κ : (a : α) → Measure β) x : Measure β),
    Tendsto (fun (n : ℕ) ↦ (s' n x : (a : β) → E) a) atTop (𝓝 (f x a))

Tactic:
refine Eventually.of_forall fun y => SimpleFunc.tendsto_approxOn hf.measurable (by simp) ?_

Premises used: MeasureTheory.StronglyMeasurable.measurable, Filter.Eventually.of_forall, MeasureTheory.SimpleFunc.tendsto_approxOn
-- 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 κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
y : β
pos : uncurry f (x, y) ∈ range (uncurry f) ∪ {0}
⊢ uncurry f (x, y) ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range (uncurry f) ∪ {0})

Tactic:
apply subset_closure

Premises used: subset_closure
-- 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 κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
y : β
⊢ uncurry f (x, y) ∈ range (uncurry f) ∪ {0}

Tactic:
simp [-uncurry_apply_pair]

Premises used: Function.uncurry_apply_pair
-- 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 κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : ¬@Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))

Tactic:
simp [f', hfx, integral_undef]

Premises used: MeasureTheory.integral_undef