awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
f_1 : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
refine :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Measurable (β := ℝ≥0∞) fun (b : α) ↦
      ((Measure.withDensity ((κ : (a : α) → Measure β) b) (f b) : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (a : α) ↦ Measure.withDensity ((κ : (a : α) → Measure β) a) (f a)

Tactic:
refine Measure.measurable_of_measurable_coe _ fun s hs => ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
f_1 : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
s : Set β
hs : MeasurableSet s
simp_rw : Measurable (β := ℝ≥0∞) fun (b : α) ↦ ∫⁻ (a : β) in s, f b a ∂(κ : (a : α) → Measure β) b
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.withDensity ((κ : (a : α) → Measure β) b) (f b) : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
simp_rw [withDensity_apply _ hs]

Premises used: MeasureTheory.withDensity_apply
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
f_1 : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ ∫⁻ (a : β) in s, f b a ∂(κ : (a : α) → Measure β) b

Tactic:
hf.setLIntegral_kernel_prod_right hs

Premises used: Measurable.setLIntegral_kernel_prod_right
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
f_1 : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ ∫⁻ (a : β) in s, f b a ∂(κ : (a : α) → Measure β) b

Tactic:
exact hf.setLIntegral_kernel_prod_right hs

Premises used: Measurable.setLIntegral_kernel_prod_right
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf : ¬Measurable (Function.uncurry f)
⊢ κ.withDensity f = 0

Tactic:
dif_neg hf

Premises used: dif_neg, ProbabilityTheory.Kernel.withDensity
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf : ¬Measurable (Function.uncurry f)
⊢ κ.withDensity f = 0

Tactic:
exact dif_neg hf

Premises used: dif_neg
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf : ¬Measurable (Function.uncurry f)
⊢ κ.withDensity f = 0

Tactic:
classical exact dif_neg hf

Premises used: dif_neg
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
rw :
  Eq.{u_2 + 1} (α := Measure β)
    (({ toFun := fun (a : α) ↦ Measure.withDensity ((κ : (a : α) → Measure β) a) (f a), measurable' := ⋯ :
            Kernel α β } :
          (a : α) → Measure β)
        a :
      Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β)
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ.withDensity f : (a : α) → Measure β) a : Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β)

Tactic:
rw [withDensity, dif_pos hf]

Premises used: dif_pos, ProbabilityTheory.Kernel.withDensity
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
⊢ Eq.{u_2 + 1} (α := Measure β)
    (({ toFun := fun (a : α) ↦ Measure.withDensity ((κ : (a : α) → Measure β) a) (f a), measurable' := ⋯ :
            Kernel α β } :
          (a : α) → Measure β)
        a :
      Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
rw :
  Eq.{u_2 + 1} (α := Measure β)
    (((if hf : Measurable (Function.uncurry f) then
              { toFun := fun (a : α) ↦ Measure.withDensity ((κ : (a : α) → Measure β) a) (f a), measurable' := ⋯ }
            else 0 :
            Kernel α β) :
          (a : α) → Measure β)
        a :
      Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β)
rw₁ rw₂ rw₃ :
  Eq.{u_2 + 1} (α := Measure β)
    (({ toFun := fun (a : α) ↦ Measure.withDensity ((κ : (a : α) → Measure β) a) (f a), measurable' := ⋯ :
            Kernel α β } :
          (a : α) → Measure β)
        a :
      Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β)
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ.withDensity f : (a : α) → Measure β) a : Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β)

Tactic:
classical
  rw [withDensity, dif_pos hf]
  rfl

Premises used: dif_pos, ProbabilityTheory.Kernel.withDensity
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
s : Set β
rw :
  ((Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s =
    ∫⁻ (b : β) in s, f a b ∂(κ : (a : α) → Measure β) a
rw₁ rw₂ : ∫⁻ (a_1 : β) in s, f a a_1 ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β) in s, f a b ∂(κ : (a : α) → Measure β) a
⊢ (((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s =
    ∫⁻ (b : β) in s, f a b ∂(κ : (a : α) → Measure β) a

Tactic:
rw [Kernel.withDensity_apply κ hf, withDensity_apply' _ s]

Premises used: ProbabilityTheory.Kernel.withDensity_apply, MeasureTheory.withDensity_apply'
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
h :
  ∀ (a : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ.withDensity g : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ.withDensity f = κ.withDensity g

Tactic:
ext a
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
a : α
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.withDensity g : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.withDensity ((κ : (a : α) → Measure β) a) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₂ h₃ :
  Eq (α := ℝ≥0∞) (((Measure.withDensity ((κ : (a : α) → Measure β) a) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.withDensity ((κ : (a : α) → Measure β) a) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.withDensity g : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Kernel.withDensity_apply _ hf, Kernel.withDensity_apply _ hg, withDensity_congr_ae (hfg a)]

Premises used: ProbabilityTheory.Kernel.withDensity_apply
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
pos :
  ∀ (hf : Measurable (Function.uncurry f)),
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ.withDensity f : (a : α) → Measure β) a)
      ((κ : (a : α) → Measure β) a)
neg :
  ∀ (hf : ¬Measurable (Function.uncurry f)),
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ.withDensity f : (a : α) → Measure β) a)
      ((κ : (a : α) → Measure β) a)
⊢ Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ.withDensity f : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)

Tactic:
by_cases hf : Measurable (Function.uncurry f)

Premises used: Measurable, Function.uncurry
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : Measurable (Function.uncurry f)
pos :
  Measure.AbsolutelyContinuous (_m0 := mβ) (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a))
    ((κ : (a : α) → Measure β) a)
⊢ Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ.withDensity f : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)

Tactic:
rw [Kernel.withDensity_apply _ hf]

Premises used: ProbabilityTheory.Kernel.withDensity_apply
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : Measurable (Function.uncurry f)
⊢ Measure.AbsolutelyContinuous (_m0 := mβ) (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a))
    ((κ : (a : α) → Measure β) a)

Tactic:
withDensity_absolutelyContinuous _ _

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : Measurable (Function.uncurry f)
⊢ Measure.AbsolutelyContinuous (_m0 := mβ) (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a))
    ((κ : (a : α) → Measure β) a)

Tactic:
exact withDensity_absolutelyContinuous _ _

Premises used: ProbabilityTheory.Kernel.withDensity_absolutelyContinuous
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : ¬Measurable (Function.uncurry f)
neg :
  Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) (((0 : Kernel α β) : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)
⊢ Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ.withDensity f : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)

Tactic:
rw [withDensity_of_not_measurable _ hf]

Premises used: ProbabilityTheory.Kernel.withDensity_of_not_measurable
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : ¬Measurable (Function.uncurry f)
⊢ Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) (((0 : Kernel α β) : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)

Tactic:
simp [Measure.AbsolutelyContinuous.zero]

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.zero
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
h :
  ∀ (a : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((κ.withDensity 1 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ.withDensity 1 = κ

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((Measure.withDensity ((κ : (a : α) → Measure β) a) (1 a) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.withDensity 1 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Kernel.withDensity_apply _ measurable_const]

Premises used: ProbabilityTheory.Kernel.withDensity_apply
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((Measure.withDensity ((κ : (a : α) → Measure β) a) (1 a) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
⊢ (κ.withDensity fun (x : α) (x_1 : β) ↦ 1) = κ

Tactic:
Kernel.withDensity_one _

Premises used: ProbabilityTheory.Kernel.withDensity_one
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
h :
  ∀ (a : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((κ.withDensity 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ.withDensity 0 = 0

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((Measure.withDensity ((κ : (a : α) → Measure β) a) (0 a) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.withDensity 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Kernel.withDensity_apply _ measurable_const]

Premises used: ProbabilityTheory.Kernel.withDensity_apply
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((Measure.withDensity ((κ : (a : α) → Measure β) a) (0 a) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
⊢ (κ.withDensity fun (x : α) (x_1 : β) ↦ 0) = 0

Tactic:
Kernel.withDensity_zero _

Premises used: ProbabilityTheory.Kernel.withDensity_zero
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
g : β → ℝ≥0∞
hg : Measurable g
rw : ∫⁻ (a_1 : β), (f a * g) a_1 ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), f a b * g b ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (b : β), g b ∂(κ.withDensity f : (a : α) → Measure β) a = ∫⁻ (b : β), f a b * g b ∂(κ : (a : α) → Measure β) a

Tactic:
rw [Kernel.withDensity_apply _ hf,
    lintegral_withDensity_eq_lintegral_mul _ (Measurable.of_uncurry_left hf) hg]

Premises used: MeasureTheory.lintegral_withDensity_eq_lintegral_mul, ProbabilityTheory.Kernel.withDensity_apply, Measurable.of_uncurry_left
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
g : β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (a_1 : β), (f a * g) a_1 ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), f a b * g b ∂(κ : (a : α) → Measure β) a

Tactic:
simp_rw [Pi.mul_apply]

Premises used: Pi.mul_apply
-- Module: Mathlib.Probability.Kernel.WithDensity
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
inst_2 : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
f_meas : Measurable (g a)
hf : Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (b : β) ↦ (↑(g a b) : ℝ≥0∞))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ.withDensity fun (a : α) (b : β) ↦ (↑(g a b) : ℝ≥0∞) : (a : α) → Measure β) a)
      fun (b : β) ↦ f b)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g a b • f b)

Tactic:
rw [Kernel.withDensity_apply, integral_withDensity_eq_integral_smul]

Premises used: integral_withDensity_eq_integral_smul, ProbabilityTheory.Kernel.withDensity_apply
-- Module: Mathlib.Probability.Kernel.WithDensity
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
inst_2 : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ Measurable (g a)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.WithDensity
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
inst_2 : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (b : β) ↦ (↑(g a b) : ℝ≥0∞))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
f : α → β → ℝ≥0∞
pos : ∀ (hf : Measurable (Function.uncurry f)), (κ + η).withDensity f = κ.withDensity f + η.withDensity f
neg : ∀ (hf : ¬Measurable (Function.uncurry f)), (κ + η).withDensity f = κ.withDensity f + η.withDensity f
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f

Tactic:
by_cases hf : Measurable (Function.uncurry f)

Premises used: Measurable, Function.uncurry
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
pos :
  ∀ (a : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((((κ + η).withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ.withDensity f + η.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f

Tactic:
ext a s
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
a : α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((((κ + η).withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.withDensity f + η.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [Kernel.withDensity_apply _ hf, coe_add, Pi.add_apply, withDensity_add_measure,
      Measure.add_apply]

Premises used: ProbabilityTheory.Kernel.coe_add, MeasureTheory.Measure.add_apply, Pi.add_apply, ProbabilityTheory.Kernel.withDensity_apply, MeasureTheory.withDensity_add_measure
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
neg : 0 = HAdd.hAdd (α := Kernel α β) 0 0
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f

Tactic:
simp_rw [withDensity_of_not_measurable _ hf]

Premises used: ProbabilityTheory.Kernel.withDensity_of_not_measurable
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
neg neg₁ : Eq (α := Kernel α β) 0 0
⊢ 0 = HAdd.hAdd (α := Kernel α β) 0 0

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
pos :
  ∀ (hf : Measurable (Function.uncurry f)), (Kernel.sum κ).withDensity f = Kernel.sum fun (i : ι) ↦ (κ i).withDensity f
neg :
  ∀ (hf : ¬Measurable (Function.uncurry f)), (Kernel.sum κ).withDensity f = Kernel.sum fun (i : ι) ↦ (κ i).withDensity f
⊢ (Kernel.sum κ).withDensity f = Kernel.sum fun (i : ι) ↦ (κ i).withDensity f

Tactic:
by_cases hf : Measurable (Function.uncurry f)

Premises used: Measurable, Function.uncurry
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
pos :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := Measure β) (((Kernel.sum κ).withDensity f : (a : α) → Measure β) a : Measure β)
      ((Kernel.sum fun (i : ι) ↦ (κ i).withDensity f : (a : α) → Measure β) a : Measure β)
⊢ (Kernel.sum κ).withDensity f = Kernel.sum fun (i : ι) ↦ (κ i).withDensity f

Tactic:
ext1 a
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
a : α
pos :
  Eq.{u_2 + 1} (α := Measure β) (((Kernel.sum κ).withDensity f : (a : α) → Measure β) a : Measure β)
    (Measure.sum fun (n : ι) ↦ ((κ n).withDensity f : (a : α) → Measure β) a : Measure β)
pos₁ :
  Eq (α := Measure β) (Measure.withDensity ((Kernel.sum κ : (a : α) → Measure β) a) (f a))
    (Measure.sum fun (n : ι) ↦ Measure.withDensity ((κ n : (a : α) → Measure β) a) (f a))
pos₂ :
  Eq (α := Measure β) (Measure.withDensity (Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) a) (f a))
    (Measure.sum fun (n : ι) ↦ Measure.withDensity ((κ n : (a : α) → Measure β) a) (f a))
⊢ Eq.{u_2 + 1} (α := Measure β) (((Kernel.sum κ).withDensity f : (a : α) → Measure β) a : Measure β)
    ((Kernel.sum fun (i : ι) ↦ (κ i).withDensity f : (a : α) → Measure β) a : Measure β)

Tactic:
simp_rw [sum_apply, Kernel.withDensity_apply _ hf, sum_apply,
      withDensity_sum (fun n => κ n a) (f a)]

Premises used: MeasureTheory.withDensity_sum, ProbabilityTheory.Kernel.withDensity_apply, ProbabilityTheory.Kernel.sum_apply, DFunLike.coe