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)
⊢ Tendsto f' atTop (𝓝 fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y)

Tactic:
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
        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
      simp only [f', 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) n
        exact fun n => Eventually.of_forall fun y =>
          SimpleFunc.norm_approxOn_zero_le hf.measurable (by simp) (x, y) n
      · refine Eventually.of_forall fun y => SimpleFunc.tendsto_approxOn hf.measurable (by simp) ?_
        apply subset_closure
        simp [-uncurry_apply_pair]
    · simp [f', hfx, integral_undef]
-- 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)
h2f' : Tendsto f' atTop (𝓝 fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y)
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y

Tactic:
stronglyMeasurable_of_tendsto _ hf' h2f'

Premises used: stronglyMeasurable_of_tendsto
-- 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)
h2f' : Tendsto f' atTop (𝓝 fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y)
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y

Tactic:
exact stronglyMeasurable_of_tendsto _ hf' h2f'

Premises used: stronglyMeasurable_of_tendsto
-- 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 f
⊢ StronglyMeasurable (uncurry (Function.curry f))

Tactic:
rw [← uncurry_curry f] at hf

Premises used: Function.uncurry_curry
-- 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 (Function.curry f))
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f (x, y)

Tactic:
hf.integral_kernel_prod_right

Premises used: MeasureTheory.StronglyMeasurable.integral_kernel_prod_right
-- 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 (Function.curry f))
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f (x, y)

Tactic:
exact hf.integral_kernel_prod_right

Premises used: MeasureTheory.StronglyMeasurable.integral_kernel_prod_right
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : β × γ → E
hf : StronglyMeasurable f
x :
  StronglyMeasurable.{u_2, u_4} (α := β) (β := E)
    ((fun (x : α × β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) x) fun (y : γ) ↦
          (fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)) (x, y)) ∘
      fun (x : β) ↦ (a, x))
⊢ StronglyMeasurable.{u_2, u_4} (β := E) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y)

Tactic:
change
    StronglyMeasurable
      ((fun x => ∫ y, (fun u : (α × β) × γ => f (u.1.2, u.2)) (x, y) ∂η x) ∘ fun x => (a, x))

Premises used: Function.comp, Prod.mk, Prod.fst, MeasureTheory.integral, MeasureTheory.StronglyMeasurable, Prod.snd, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : β × γ → E
hf : StronglyMeasurable f
apply :
  StronglyMeasurable (β := E) fun (x : α × β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) x) fun (y : γ) ↦ (fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)) (x, y)
⊢ StronglyMeasurable.{u_2, u_4} (α := β) (β := E)
    ((fun (x : α × β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) x) fun (y : γ) ↦
          (fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)) (x, y)) ∘
      fun (x : β) ↦ (a, x))

Tactic:
apply StronglyMeasurable.comp_measurable _ (measurable_prodMk_left (m := mα))

Premises used: MeasureTheory.StronglyMeasurable.comp_measurable, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : β × γ → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable (β := E) fun (x : α × β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) x) fun (y : γ) ↦
      (f ∘ fun (a : (α × β) × γ) ↦ (a.1.2, a.2)) (x, y)

Tactic:
have := MeasureTheory.StronglyMeasurable.integral_kernel_prod_right' (κ := η)
      (hf.comp_measurable (measurable_fst.snd.prodMk measurable_snd))
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : β × γ → E
hf : StronglyMeasurable f
this :
  StronglyMeasurable (β := E) fun (x : α × β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) x) fun (y : γ) ↦
      (f ∘ fun (a : (α × β) × γ) ↦ (a.1.2, a.2)) (x, y)
⊢ StronglyMeasurable (β := E) fun (x : α × β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) x) fun (y : γ) ↦ (fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)) (x, y)

Tactic:
simpa using this
-- 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)
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (y : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) y) fun (x : β) ↦ f x y

Tactic:
(hf.comp_measurable measurable_swap).integral_kernel_prod_right'

Premises used: MeasureTheory.StronglyMeasurable.integral_kernel_prod_right', MeasureTheory.StronglyMeasurable.comp_measurable, measurable_swap
-- 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 f
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (y : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) y) fun (x : β) ↦ f (x, y)

Tactic:
(hf.comp_measurable measurable_swap).integral_kernel_prod_right'

Premises used: MeasureTheory.StronglyMeasurable.integral_kernel_prod_right', MeasureTheory.StronglyMeasurable.comp_measurable, measurable_swap, Prod.swap
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
y :
  StronglyMeasurable.{u_2, u_4} (α := β) (β := E)
    ((fun (y : α × β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) y) fun (x : γ) ↦
          (fun (u : γ × α × β) ↦ f (u.1, u.2.2)) (x, y)) ∘
      fun (x : β) ↦ (a, x))
⊢ StronglyMeasurable.{u_2, u_4} (β := E) fun (y : β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, y)) fun (x : γ) ↦ f (x, y)

Tactic:
change
    StronglyMeasurable
      ((fun y => ∫ x, (fun u : γ × α × β => f (u.1, u.2.2)) (x, y) ∂η y) ∘ fun x => (a, x))

Premises used: Function.comp, Prod.mk, Prod.fst, MeasureTheory.integral, MeasureTheory.StronglyMeasurable, Prod.snd, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
apply :
  StronglyMeasurable (β := E) fun (y : α × β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) y) fun (x : γ) ↦ (fun (u : γ × α × β) ↦ f (u.1, u.2.2)) (x, y)
⊢ StronglyMeasurable.{u_2, u_4} (α := β) (β := E)
    ((fun (y : α × β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) y) fun (x : γ) ↦
          (fun (u : γ × α × β) ↦ f (u.1, u.2.2)) (x, y)) ∘
      fun (x : β) ↦ (a, x))

Tactic:
apply StronglyMeasurable.comp_measurable _ (measurable_prodMk_left (m := mα))

Premises used: MeasureTheory.StronglyMeasurable.comp_measurable, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable (β := E) fun (y : α × β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) y) fun (x : γ) ↦ (f ∘ fun (a : γ × α × β) ↦ (a.1, a.2.2)) (x, y)

Tactic:
have := MeasureTheory.StronglyMeasurable.integral_kernel_prod_left' (κ := η)
      (hf.comp_measurable (measurable_fst.prodMk measurable_snd.snd))
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
this :
  StronglyMeasurable (β := E) fun (y : α × β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) y) fun (x : γ) ↦ (f ∘ fun (a : γ × α × β) ↦ (a.1, a.2.2)) (x, y)
⊢ StronglyMeasurable (β := E) fun (y : α × β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) y) fun (x : γ) ↦ (fun (u : γ × α × β) ↦ f (u.1, u.2.2)) (x, y)

Tactic:
simpa using this
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ∅)

Tactic:
simp only [preimage_empty, measure_empty, measurable_const]

Premises used: MeasureTheory.measure_empty, Set.preimage_empty, measurable_const
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
ht :
  Membership.mem (γ := Set (Set (α × β)))
    (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t}) t
⊢ ∃ (a : Set α), MeasurableSet a ∧ ∃ (b : Set β), MeasurableSet b ∧ a ×ˢ b = t

Tactic:
simp only [Set.mem_image2, Set.mem_setOf_eq] at ht

Premises used: Set.mem_image2, Set.mem_setOf_eq
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
ht : ∃ (a : Set α), MeasurableSet a ∧ ∃ (b : Set β), MeasurableSet b ∧ a ×ˢ b = t
basic :
  ∀ (t₁ : Set α) (ht₁ : MeasurableSet t₁) (t₂ : Set β) (ht₂ : MeasurableSet t₂),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)

Tactic:
obtain ⟨t₁, ht₁, t₂, ht₂, rfl⟩ := ht

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
basic :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)

Tactic:
simp_rw [mk_preimage_prod_right_eq_if]

Premises used: Set.mk_preimage_prod_right_eq_if
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
h :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅) : ℝ≥0∞)
      (if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0 : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅))
    fun (a : α) ↦ if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0

Tactic:
ext1 a
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
pos :
  a ∈ t₁ →
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞)
neg : a ∉ t₁ → Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) ∅) 0
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅) : ℝ≥0∞)
    (if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0 : ℝ≥0∞)

Tactic:
split_ifs
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
h : a ∈ t₁
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
h : a ∉ t₁
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) ∅) 0

Tactic:
measure_empty

Premises used: MeasureTheory.measure_empty
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
h : a ∈ t₁
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞)

Tactic:
exacts [rfl, measure_empty]

Premises used: MeasureTheory.measure_empty, rfl
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅))
    fun (a : α) ↦ if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0

Tactic:
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]
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
h_eq_ite :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅))
    fun (a : α) ↦ if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0
basic :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅)

Tactic:
rw [h_eq_ite]
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
h_eq_ite :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅))
    fun (a : α) ↦ if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0

Tactic:
Measurable.ite ht₁ (Kernel.measurable_coe κ ht₂) measurable_const

Premises used: Measurable.ite, ProbabilityTheory.Kernel.measurable_coe, measurable_const
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
h_eq_ite :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅))
    fun (a : α) ↦ if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0

Tactic:
exact Measurable.ite ht₁ (Kernel.measurable_coe κ ht₂) measurable_const

Premises used: Measurable.ite, ProbabilityTheory.Kernel.measurable_coe, measurable_const