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 β
inst : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
neg : Eq (α := Kernel α β) 0 (Kernel.sum fun (i : ι) ↦ 0)
⊢ (Kernel.sum κ).withDensity f = Kernel.sum fun (i : ι) ↦ (κ i).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
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ Eq (α := Kernel α β) 0 (Kernel.sum fun (i : ι) ↦ 0)

Tactic:
sum_zero.symm

Premises used: ProbabilityTheory.Kernel.sum_zero, Eq.symm
-- 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)
⊢ Eq (α := Kernel α β) 0 (Kernel.sum fun (i : ι) ↦ 0)

Tactic:
exact sum_zero.symm

Premises used: ProbabilityTheory.Kernel.sum_zero, Eq.symm
-- 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)
h :
  ∀ (a : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((κ.withDensity (f + g) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ.withDensity f + κ.withDensity g : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ.withDensity (f + g) = κ.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)
a : α
s : Set β
h_1 : MeasurableSet s
h : Measurable (g a)
h₁ : Measurable (Function.uncurry (f + g))
⊢ Eq (α := ℝ≥0∞) ((((κ.withDensity (f + g) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.withDensity f + κ.withDensity g : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [coe_add, Pi.add_apply, Kernel.withDensity_apply _ hf, Kernel.withDensity_apply _ hg,
    Kernel.withDensity_apply, Pi.add_apply, MeasureTheory.withDensity_add_right]

Premises used: ProbabilityTheory.Kernel.coe_add, Pi.add_apply, ProbabilityTheory.Kernel.withDensity_apply, MeasureTheory.withDensity_add_right
-- 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)
a : α
s : Set β
h : MeasurableSet s
⊢ Measurable (g a)

Tactic:
fun_prop
-- 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)
a : α
s : Set β
h : MeasurableSet s
⊢ Measurable (Function.uncurry (f + g))

Tactic:
hf.add hg

Premises used: Measurable.add
-- 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)
a : α
s : Set β
h : MeasurableSet s
⊢ Measurable (Function.uncurry (f + g))

Tactic:
exact hf.add hg

Premises used: Measurable.add
-- 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 : α), g a ≤ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] f a
rw : κ.withDensity ((fun (a : α) (x : β) ↦ f a x - g a x) + g) = κ.withDensity f
rw₁ : Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : β) ↦ f a x - g a x)
⊢ (κ.withDensity fun (a : α) (x : β) ↦ f a x - g a x) + κ.withDensity g = κ.withDensity f

Tactic:
rw [← withDensity_add_right _ hg]

Premises used: ProbabilityTheory.Kernel.withDensity_add_right
-- 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 : α), g a ≤ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] f a
⊢ Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : β) ↦ f a x - g a x)

Tactic:
hf.sub hg

Premises used: Measurable.sub
-- 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 : α), g a ≤ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] f a
⊢ Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : β) ↦ f a x - g a x)

Tactic:
exact hf.sub hg

Premises used: Measurable.sub
-- 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 : α), g a ≤ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] f a
⊢ κ.withDensity ((fun (a : α) (x : β) ↦ f a x - g a x) + g) = κ.withDensity f

Tactic:
withDensity_congr_ae κ ((hf.sub hg).add hg) hf (fun a ↦ ?_)

Premises used: Measurable.sub, Measurable.add, ProbabilityTheory.Kernel.withDensity_congr_ae
-- 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 : α), g a ≤ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] f a
refine :
  ∀ (a : α),
    HAdd.hAdd (α := α → β → ℝ≥0∞) (fun (a : α) (x : β) ↦ f a x - g a x) g
        a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)]
      f a
⊢ κ.withDensity ((fun (a : α) (x : β) ↦ f a x - g a x) + g) = κ.withDensity f

Tactic:
refine withDensity_congr_ae κ ((hf.sub hg).add hg) hf (fun 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 : α), g a ≤ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] f a
a : α
h : ∀ (x : β) (hx : g a x ≤ f a x), HAdd.hAdd (α := α → β → ℝ≥0∞) (fun (a : α) (x : β) ↦ f a x - g a x) g a x = f a x
⊢ HAdd.hAdd (α := α → β → ℝ≥0∞) (fun (a : α) (x : β) ↦ f a x - g a x) g
      a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)]
    f a

Tactic:
filter_upwards [hfg a] with x hx
-- 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 : α), g a ≤ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] f a
a : α
x : β
hx : g a x ≤ f a x
h : HAdd.hAdd (α := (x : β) → ℝ≥0∞) (fun (x : β) ↦ f a x - g a x) (g a) x = f a x
h₁ : f a x - g a x + g a x = f a x
h₂ h₃ h₄ h₅ : g a x ≤ f a x
⊢ HAdd.hAdd (α := α → β → ℝ≥0∞) (fun (a : α) (x : β) ↦ f a x - g a x) g a x = f a x

Tactic:
rwa [Pi.add_apply, Pi.add_apply, tsub_add_cancel_iff_le]

Premises used: tsub_add_cancel_iff_le, Pi.add_apply
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
⊢ ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a

Tactic:
have h_sum_a : ∀ a, Summable fun n => f n a := fun a => Pi.summable.mpr fun b => ENNReal.summable
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
⊢ Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n

Tactic:
have h_sum : Summable fun n => f n := Pi.summable.mpr h_sum_a
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
h :
  ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((κ.withDensity (∑' (n : ι), f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((Kernel.sum fun (n : ι) ↦ κ.withDensity (f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
        ℝ≥0∞)
⊢ κ.withDensity (∑' (n : ι), f n) = Kernel.sum fun (n : ι) ↦ κ.withDensity (f n)

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
h :
  ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂(κ : (a : α) → Measure β) a =
    ∑' (n : ι), (((κ.withDensity (f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
rw : Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry (∑' (n : ι), f n))
⊢ Eq (α := ℝ≥0∞)
    ((((κ.withDensity (∑' (n : ι), f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (n : ι) ↦ κ.withDensity (f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
rw [sum_apply' _ a hs, Kernel.withDensity_apply' κ _ a s]

Premises used: ProbabilityTheory.Kernel.withDensity_apply', ProbabilityTheory.Kernel.sum_apply'
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
h : ∀ (p : α × β), Eq (α := ℝ≥0∞) (Function.uncurry (∑' (n : ι), f n) p) ((∑' (n : ι), Function.uncurry (f n)) p)
⊢ Eq (α := α × β → ℝ≥0∞) (Function.uncurry (∑' (n : ι), f n)) (∑' (n : ι), Function.uncurry (f n))

Tactic:
ext1 p
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
h : Eq (α := ℝ≥0∞) ((∑' (n : ι), f n) p.1 p.2) ((∑' (n : ι), fun (p : α × β) ↦ f n p.1 p.2) p)
⊢ Eq (α := ℝ≥0∞) (Function.uncurry (∑' (n : ι), f n) p) ((∑' (n : ι), Function.uncurry (f n)) p)

Tactic:
simp only [Function.uncurry_def]

Premises used: Function.uncurry_def
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
h : Summable (α := (x : α × β) → ℝ≥0∞) fun (n : ι) (p : α × β) ↦ f n p.1 p.2
⊢ Eq (α := ℝ≥0∞) ((∑' (n : ι), f n) p.1 p.2) ((∑' (n : ι), fun (p : α × β) ↦ f n p.1 p.2) p)

Tactic:
rw [tsum_apply h_sum, tsum_apply (h_sum_a _), tsum_apply]

Premises used: tsum_apply
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
⊢ Summable (α := (x : α × β) → ℝ≥0∞) fun (n : ι) (p : α × β) ↦ f n p.1 p.2

Tactic:
Pi.summable.mpr fun p => ENNReal.summable

Premises used: Iff.mpr, ENNReal.summable, Pi.summable
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
⊢ Summable (α := (x : α × β) → ℝ≥0∞) fun (n : ι) (p : α × β) ↦ f n p.1 p.2

Tactic:
exact Pi.summable.mpr fun p => ENNReal.summable

Premises used: Iff.mpr, ENNReal.summable, Pi.summable
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := α × β → ℝ≥0∞) (Function.uncurry (∑' (n : ι), f n)) (∑' (n : ι), Function.uncurry (f n))

Tactic:
have : Function.uncurry (∑' n, f n) = ∑' n, Function.uncurry (f n) := by
      ext1 p
      simp only [Function.uncurry_def]
      rw [tsum_apply h_sum, tsum_apply (h_sum_a _), tsum_apply]
      exact Pi.summable.mpr fun p => ENNReal.summable
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
this : Eq (α := α × β → ℝ≥0∞) (Function.uncurry (∑' (n : ι), f n)) (∑' (n : ι), Function.uncurry (f n))
rw : Measurable (α := α × β) (β := ℝ≥0∞) (∑' (n : ι), Function.uncurry (f n))
⊢ Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry (∑' (n : ι), f n))

Tactic:
rw [this]
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
this : Eq (α := α × β → ℝ≥0∞) (Function.uncurry (∑' (n : ι), f n)) (∑' (n : ι), Function.uncurry (f n))
⊢ Measurable (α := α × β) (β := ℝ≥0∞) (∑' (n : ι), Function.uncurry (f n))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
e_f : ∀ (b : β), Eq (α := ℝ≥0∞) ((∑' (n : ι), f n) a b) (∑' (n : ι), (fun (b : β) ↦ f n a b) b)
⊢ ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s, ∑' (n : ι), (fun (b : β) ↦ f n a b) b ∂(κ : (a : α) → Measure β) a

Tactic:
congr with b
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
b : β
e_f : Eq (α := ℝ≥0∞) ((∑' (i : ι), f i a) b) (∑' (n : ι), (fun (b : β) ↦ f n a b) b)
e_f₁ e_f₂ : Eq (α := ℝ≥0∞) (∑' (i : ι), f i a b) (∑' (n : ι), (fun (b : β) ↦ f n a b) b)
⊢ Eq (α := ℝ≥0∞) ((∑' (n : ι), f n) a b) (∑' (n : ι), (fun (b : β) ↦ f n a b) b)

Tactic:
rw [tsum_apply h_sum, tsum_apply (h_sum_a a)]

Premises used: tsum_apply
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s, ∑' (n : ι), (fun (b : β) ↦ f n a b) b ∂(κ : (a : α) → Measure β) a

Tactic:
have : ∫⁻ b in s, (∑' n, f n) a b ∂κ a = ∫⁻ b in s, ∑' n, (fun b => f n a b) b ∂κ a := by
    congr with b
    rw [tsum_apply h_sum, tsum_apply (h_sum_a a)]
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
this :
  ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s, ∑' (n : ι), (fun (b : β) ↦ f n a b) b ∂(κ : (a : α) → Measure β) a
n : ι
⊢ AEMeasurable (β := ℝ≥0∞) (_m := mβ) (fun (b : β) ↦ f n a b) (Measure.restrict ((κ : (a : α) → Measure β) a) s)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
this :
  ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s, ∑' (n : ι), (fun (b : β) ↦ f n a b) b ∂(κ : (a : α) → Measure β) a
h :
  Eq (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a_1 : β) in s, f i a a_1 ∂(κ : (a : α) → Measure β) a)
    (∑' (n : ι), (((κ.withDensity (f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
⊢ ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂(κ : (a : α) → Measure β) a =
    ∑' (n : ι), (((κ.withDensity (f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
rw [this, lintegral_tsum fun n => by fun_prop]

Premises used: MeasureTheory.lintegral_tsum
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
this :
  ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s, ∑' (n : ι), (fun (b : β) ↦ f n a b) b ∂(κ : (a : α) → Measure β) a
h :
  ∀ (n : ι),
    ∫⁻ (a_1 : β) in s, f n a a_1 ∂(κ : (a : α) → Measure β) a =
      (((κ.withDensity (f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a_1 : β) in s, f i a a_1 ∂(κ : (a : α) → Measure β) a)
    (∑' (n : ι), (((κ.withDensity (f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)

Tactic:
congr with n
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
a : α
s : Set β
hs : MeasurableSet s
this :
  ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s, ∑' (n : ι), (fun (b : β) ↦ f n a b) b ∂(κ : (a : α) → Measure β) a
n : ι
h h₁ : ∫⁻ (a_1 : β) in s, f n a a_1 ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β) in s, f n a b ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (a_1 : β) in s, f n a a_1 ∂(κ : (a : α) → Measure β) a =
    (((κ.withDensity (f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
rw [Kernel.withDensity_apply' _ (hf n) a s]

Premises used: ProbabilityTheory.Kernel.withDensity_apply'
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
pos : ∀ (hf : Measurable (Function.uncurry f)), IsFiniteKernel (κ.withDensity f)
neg : ∀ (hf : ¬Measurable (Function.uncurry f)), IsFiniteKernel (κ.withDensity f)
⊢ IsFiniteKernel (κ.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 β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
a : α
rw : ∫⁻ (b : β) in Set.univ, f a b ∂(κ : (a : α) → Measure β) a ≤ B * κ.bound
⊢ (((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ B * κ.bound

Tactic:
rw [Kernel.withDensity_apply' κ hf a Set.univ]

Premises used: Set.univ, ProbabilityTheory.Kernel.withDensity_apply'