awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
⊢ f = ∑' (n : ℕ), fs n
have h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
Tactic: have h_sum_a : ∀ a, Summable fun n => fs n a :=
      fun _ => Pi.summable.mpr fun _ => ENNReal.summable
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
⊢ f = ∑' (n : ℕ), fs n
have h : ∀ (a : α) (b : β), f a b = (∑' (n : ℕ), fs n) a b
Tactic: ext a b : 2
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
⊢ f a b = (∑' (n : ℕ), fs n) a b
have h : f a b = Filter.liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, fs i a b) Filter.atTop
Tactic: rw [tsum_apply (Pi.summable.mpr h_sum_a), tsum_apply (h_sum_a a),
      ENNReal.tsum_eq_liminf_sum_nat]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
n : ℕ
hn : ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range (n + 1), fs i a b = min (f a b) (↑(n + 1) : ℝ≥0∞)
have succ : min (f a b) (↑n : ℝ≥0∞) + fs n a b = min (f a b) (↑(n + 1) : ℝ≥0∞)
Tactic: rw [Finset.sum_range_succ, hn]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
n : ℕ
⊢ ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
have zero : ∑ i ∈ Finset.range 0, fs i a b = min (f a b) (↑0 : ℝ≥0∞)
Tactic: induction n with
      | zero => simp
      | succ n hn =>
        rw [Finset.sum_range_succ, hn]
        simp [fs]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
n : ℕ
zero : ∑ i ∈ Finset.range 0, fs i a b = min (f a b) (↑0 : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
have succ : ∀ (n : ℕ) (hn : ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)),
  ∑ i ∈ Finset.range (n + 1), fs i a b = min (f a b) (↑(n + 1) : ℝ≥0∞)
Tactic: induction n with
      | zero => simp
      | succ n hn =>
        rw [Finset.sum_range_succ, hn]
        simp [fs]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
⊢ f a b = Filter.liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, fs i a b) Filter.atTop
have h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
Tactic: have h_finsetSum : ∀ n, ∑ i ∈ Finset.range n, fs i a b = min (f a b) n := fun n ↦ by
      induction n with
      | zero => simp
      | succ n hn =>
        rw [Finset.sum_range_succ, hn]
        simp [fs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
⊢ f a b = Filter.liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, fs i a b) Filter.atTop
have h : f a b = Filter.liminf (fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)) Filter.atTop
Tactic: simp_rw [h_finsetSum]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
⊢ f a b = Filter.liminf (fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)) Filter.atTop
have h : Filter.Tendsto (fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)) Filter.atTop (nhds (f a b))
Tactic: refine (Filter.Tendsto.liminf_eq ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
⊢ Filter.Tendsto (fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)) Filter.atTop (nhds (f a b))
have h : Filter.EventuallyEq (β := ℝ≥0∞) Filter.atTop (fun (x : ℕ) ↦ f a b) fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)
Tactic: refine Filter.Tendsto.congr' ?_ tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
⊢ Filter.EventuallyEq (β := ℝ≥0∞) Filter.atTop (fun (x : ℕ) ↦ f a b) fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)
have h : ∃ (a_1 : ℕ), ∀ b_1 ≥ a_1, f a b = min (f a b) (↑b_1 : ℝ≥0∞)
Tactic: rw [Filter.EventuallyEq, Filter.eventually_atTop]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
⊢ IsSFiniteKernel (κ.withDensity f)
have hf_eq_tsum : f = ∑' (n : ℕ), fs n
Tactic: have hf_eq_tsum : f = ∑' n, fs n := by
    have h_sum_a : ∀ a, Summable fun n => fs n a :=
      fun _ => Pi.summable.mpr fun _ => ENNReal.summable
    ext a b : 2
    rw [tsum_apply (Pi.summable.mpr h_sum_a), tsum_apply (h_sum_a a),
      ENNReal.tsum_eq_liminf_sum_nat]
    have h_finsetSum : ∀ n, ∑ i ∈ Finset.range n, fs i a b = min (f a b) n := fun n ↦ by
      induction n with
      | zero => simp
      | succ n hn =>
        rw [Finset.sum_range_succ, hn]
        simp [fs]
    simp_rw [h_finsetSum]
    refine (Filter.Tendsto.liminf_eq ?_).symm
    refine Filter.Tendsto.congr' ?_ tendsto_const_nhds
    rw [Filter.EventuallyEq, Filter.eventually_atTop]
    exact ⟨⌈(f a b).toReal⌉₊, fun n hn => (min_eq_left (h_le a b n hn)).symm⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
⊢ IsSFiniteKernel (κ.withDensity f)
have pos : IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (Kernel.sum fun (n : ℕ) ↦ κ.withDensity (fs n))
Tactic: rw [hf_eq_tsum, withDensity_tsum _ fun n : ℕ => _]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
pos : IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (Kernel.sum fun (n : ℕ) ↦ κ.withDensity (fs n))
⊢ IsSFiniteKernel (κ.withDensity f)
have rw : ∀ (n : ℕ), Measurable (Function.uncurry (fs n))
Tactic: rw [hf_eq_tsum, withDensity_tsum _ fun n : ℕ => _]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (Kernel.sum fun (n : ℕ) ↦ κ.withDensity (fs n))
have pos : ∀ (n : ℕ), IsSFiniteKernel (κ.withDensity (fs n))
Tactic: refine isSFiniteKernel_sum (hκs := fun n => ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
⊢ IsSFiniteKernel (κ.withDensity (fs n))
have pos : IsFiniteKernel (κ.withDensity (fs n))
Tactic: suffices IsFiniteKernel (withDensity κ (fs n)) by infer_instance
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
⊢ IsFiniteKernel (κ.withDensity (fs n))
have pos : ∀ (a : α) (b : β), fs n a b ≤ (↑((fun (x1 x2 : ℝ≥0) ↦ x1 + x2) (↑n : ℝ≥0) 1) : ℝ≥0∞)
Tactic: refine isFiniteKernel_withDensity_of_bounded _ (ENNReal.coe_ne_top : ↑n + 1 ≠ ∞) fun a b => ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
a : α
b : β
⊢ fs n a b ≤ (↑(HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞)
have pos : fs n a b ≤ (↑(n + 1) : ℝ≥0∞)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
a : α
b : β
⊢ HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1 = (↑(n + 1) : ℝ≥0∞)
have norm_cast : n + 1 = n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
a : α
b : β
⊢ fs n a b ≤ (↑(n + 1) : ℝ≥0∞)
have fs₁ : HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1 = (↑(n + 1) : ℝ≥0∞)
Tactic: calc
    fs n a b ≤ min (f a b) (n + 1) := tsub_le_self
    _ ≤ n + 1 := min_le_right _ _
    _ = ↑(n + 1) := by norm_cast
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
⊢ κ.withDensity f = Kernel.sum fun (i : ℕ) ↦ (κ.seq i).withDensity f
have rw : κ.withDensity f = (Kernel.sum κ.seq).withDensity f
Tactic: rw [← withDensity_kernel_sum _ _]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
⊢ κ.withDensity f = (Kernel.sum κ.seq).withDensity f
have e_κ : κ = Kernel.sum κ.seq
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
⊢ IsSFiniteKernel (κ.withDensity f)
have h_eq_sum : κ.withDensity f = Kernel.sum fun (i : ℕ) ↦ (κ.seq i).withDensity f
Tactic: have h_eq_sum : withDensity κ f = Kernel.sum fun i => withDensity (seq κ i) f := by
    rw [← withDensity_kernel_sum _ _]
    congr
    exact (kernel_sum_seq κ).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
h_eq_sum : κ.withDensity f = Kernel.sum fun (i : ℕ) ↦ (κ.seq i).withDensity f
⊢ IsSFiniteKernel (κ.withDensity f)
have rw : IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (Kernel.sum fun (i : ℕ) ↦ (κ.seq i).withDensity f)
Tactic: rw [h_eq_sum]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
⊢ (κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞) * g a x) =
    (κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g
have h : ∀ (a : α),
  Eq.{u_2 + 1} (α := Measure β)
    ((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞) * g a x : (a : α) → Measure β) a : Measure β)
    (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a : Measure β)
Tactic: ext a : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ Eq.{u_2 + 1} (α := Measure β)
    ((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞) * g a x : (a : α) → Measure β) a : Measure β)
    (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a : Measure β)
have h : Eq.{u_2 + 1} (α := Measure β)
  (Measure.withDensity ((κ : (a : α) → Measure β) a) fun (x : β) ↦ (↑(f a x) : ℝ≥0∞) * g a x)
  (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a)
Tactic: rw [Kernel.withDensity_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
h :
  Eq.{u_2 + 1} (α := Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a) fun (x : β) ↦ (↑(f a x) : ℝ≥0∞) * g a x)
    (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a)
⊢ Eq.{u_2 + 1} (α := Measure β)
    ((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞) * g a x : (a : α) → Measure β) a : Measure β)
    (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a : Measure β)
have h₁ : Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞) * g a x)
Tactic: rw [Kernel.withDensity_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ Eq.{u_2 + 1} (α := Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a) fun (x : β) ↦ (↑(f a x) : ℝ≥0∞) * g a x)
    (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a)
have h : Eq (α := Measure β)
  (Measure.withDensity ((κ : (a : α) → Measure β) a)
    (HMul.hMul (α := (x : β) → ℝ≥0∞) (fun (x : β) ↦ (↑(f a x) : ℝ≥0∞)) fun (x : β) ↦ g a x))
  (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a)
Tactic: change (Measure.withDensity (κ a) ((fun x ↦ (f a x : ℝ≥0∞)) * (fun x ↦ (g a x : ℝ≥0∞)))) =
      (withDensity (withDensity κ fun a x ↦ f a x) g) a
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ Eq (α := Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a)
      (HMul.hMul (α := (x : β) → ℝ≥0∞) (fun (x : β) ↦ (↑(f a x) : ℝ≥0∞)) fun (x : β) ↦ g a x))
    (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a)
have h : Eq.{u_2 + 1} (α := Measure β)
  (Measure.withDensity (Measure.withDensity ((κ : (a : α) → Measure β) a) fun (x : β) ↦ (↑(f a x) : ℝ≥0∞)) fun (x : β) ↦
    g a x)
  (((κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g : (a : α) → Measure β) a)
Tactic: rw [withDensity_mul]