awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.WithDensity
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∞)
h : Filter.EventuallyEq (β := ℝ≥0∞) Filter.atTop (fun (x : ℕ) ↦ f a b) fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)
⊢ Filter.Tendsto (fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)) Filter.atTop (nhds (f a b))

Tactic:
refine Filter.Tendsto.congr' ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- Module: Mathlib.Probability.Kernel.WithDensity
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∞)
h : ∃ (a_1 : ℕ), ∀ b_1 ≥ a_1, f a b = min (f a b) (↑b_1 : ℝ≥0∞)
⊢ Filter.EventuallyEq (β := ℝ≥0∞) Filter.atTop (fun (x : ℕ) ↦ f a b) fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)

Tactic:
rw [Filter.EventuallyEq, Filter.eventually_atTop]

Premises used: Filter.EventuallyEq, Filter.eventually_atTop
-- Module: Mathlib.Probability.Kernel.WithDensity
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∞)
⊢ ∃ (a_1 : ℕ), ∀ b_1 ≥ a_1, f a b = min (f a b) (↑b_1 : ℝ≥0∞)

Tactic:
⟨⌈(f a b).toReal⌉₊, fun n hn => (min_eq_left (h_le a b n hn)).symm⟩

Premises used: ENNReal.toReal, min_eq_left, Nat.ceil, Exists.intro, Eq.symm
-- Module: Mathlib.Probability.Kernel.WithDensity
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∞)
⊢ ∃ (a_1 : ℕ), ∀ b_1 ≥ a_1, f a b = min (f a b) (↑b_1 : ℝ≥0∞)

Tactic:
exact ⟨⌈(f a b).toReal⌉₊, fun n hn => (min_eq_left (h_le a b n hn)).symm⟩
-- Module: Mathlib.Probability.Kernel.WithDensity
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

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⟩
-- Module: Mathlib.Probability.Kernel.WithDensity
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))
rw : ∀ (n : ℕ), Measurable (Function.uncurry (fs n))
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
rw [hf_eq_tsum, withDensity_tsum _ fun n : ℕ => _]

Premises used: ProbabilityTheory.Kernel.withDensity_tsum
-- Module: Mathlib.Probability.Kernel.WithDensity
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 : ℕ), Measurable (Function.uncurry (fs n))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.WithDensity
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))

Tactic:
isSFiniteKernel_sum (hκs := fun n => ?_)

Premises used: ProbabilityTheory.Kernel.isSFiniteKernel_sum
-- Module: Mathlib.Probability.Kernel.WithDensity
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 : ∀ (n : ℕ), IsSFiniteKernel (κ.withDensity (fs n))
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (Kernel.sum fun (n : ℕ) ↦ κ.withDensity (fs n))

Tactic:
refine isSFiniteKernel_sum (hκs := fun n => ?_)

Premises used: ProbabilityTheory.Kernel.isSFiniteKernel_sum
-- Module: Mathlib.Probability.Kernel.WithDensity
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 : ℕ
this : IsFiniteKernel (κ.withDensity (fs n))
⊢ IsSFiniteKernel (κ.withDensity (fs n))

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.WithDensity
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 : ℕ
pos : IsFiniteKernel (κ.withDensity (fs n))
⊢ IsSFiniteKernel (κ.withDensity (fs n))

Tactic:
suffices IsFiniteKernel (withDensity κ (fs n)) by infer_instance
-- Module: Mathlib.Probability.Kernel.WithDensity
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))

Tactic:
isFiniteKernel_withDensity_of_bounded _ (ENNReal.coe_ne_top : ↑n + 1 ≠ ∞) fun a b => ?_

Premises used: ProbabilityTheory.Kernel.isFiniteKernel_withDensity_of_bounded, ENNReal.coe_ne_top
-- Module: Mathlib.Probability.Kernel.WithDensity
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 : ℕ
pos : ∀ (a : α) (b : β), fs n a b ≤ (↑((fun (x1 x2 : ℝ≥0) ↦ x1 + x2) (↑n : ℝ≥0) 1) : ℝ≥0∞)
⊢ IsFiniteKernel (κ.withDensity (fs n))

Tactic:
refine isFiniteKernel_withDensity_of_bounded _ (ENNReal.coe_ne_top : ↑n + 1 ≠ ∞) fun a b => ?_

Premises used: ProbabilityTheory.Kernel.isFiniteKernel_withDensity_of_bounded, ENNReal.coe_ne_top
-- Module: Mathlib.Probability.Kernel.WithDensity
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 : β
pos : fs n a b ≤ (↑(n + 1) : ℝ≥0∞)
⊢ fs n a b ≤ (↑(HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Kernel.WithDensity
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 ≤ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1)

Tactic:
tsub_le_self

Premises used: tsub_le_self
-- Module: Mathlib.Probability.Kernel.WithDensity
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 : β
⊢ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) ≤ HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1

Tactic:
min_le_right _ _

Premises used: min_le_right
-- Module: Mathlib.Probability.Kernel.WithDensity
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 : β
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : n + 1 = n + 1
⊢ HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1 = (↑(n + 1) : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Kernel.WithDensity
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₁ : HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1 = (↑(n + 1) : ℝ≥0∞)
⊢ fs n a b ≤ (↑(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

Premises used: Nat.cast, tsub_le_self, HAdd.hAdd, min_le_right, OfNat.ofNat, Min.min
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
rw : κ.withDensity f = (Kernel.sum κ.seq).withDensity f
⊢ κ.withDensity f = Kernel.sum fun (i : ℕ) ↦ (κ.seq i).withDensity f

Tactic:
rw [← withDensity_kernel_sum _ _]

Premises used: ProbabilityTheory.Kernel.withDensity_kernel_sum
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
e_κ : κ = Kernel.sum κ.seq
⊢ κ.withDensity f = (Kernel.sum κ.seq).withDensity f

Tactic:
congr
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
⊢ κ = Kernel.sum κ.seq

Tactic:
(kernel_sum_seq κ).symm

Premises used: ProbabilityTheory.Kernel.kernel_sum_seq, Eq.symm
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
⊢ κ = Kernel.sum κ.seq

Tactic:
exact (kernel_sum_seq κ).symm

Premises used: ProbabilityTheory.Kernel.kernel_sum_seq, Eq.symm
-- Module: Mathlib.Probability.Kernel.WithDensity
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

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
-- Module: Mathlib.Probability.Kernel.WithDensity
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
rw :
  IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (Kernel.sum fun (i : ℕ) ↦ (κ.seq i).withDensity f)
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
rw [h_eq_sum]
-- Module: Mathlib.Probability.Kernel.WithDensity
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.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (Kernel.sum fun (i : ℕ) ↦ (κ.seq i).withDensity f)

Tactic:
isSFiniteKernel_sum (hκs := fun n =>
    isSFiniteKernel_withDensity_of_isFiniteKernel (seq κ n) hf_ne_top)

Premises used: ProbabilityTheory.Kernel.isSFiniteKernel_sum
-- Module: Mathlib.Probability.Kernel.WithDensity
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.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (Kernel.sum fun (i : ℕ) ↦ (κ.seq i).withDensity f)

Tactic:
exact isSFiniteKernel_sum (hκs := fun n =>
    isSFiniteKernel_withDensity_of_isFiniteKernel (seq κ n) hf_ne_top)

Premises used: ProbabilityTheory.Kernel.isSFiniteKernel_sum
-- 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
⊢ IsSFiniteKernel (κ.withDensity fun (a : α) (b : β) ↦ (↑(f a b) : ℝ≥0∞))

Tactic:
IsSFiniteKernel.withDensity κ fun _ _ => ENNReal.coe_ne_top

Premises used: ProbabilityTheory.Kernel.IsSFiniteKernel.withDensity, ENNReal.coe_ne_top
-- Module: Mathlib.Probability.Kernel.WithDensity
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)
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 β)
⊢ (κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞) * g a x) =
    (κ.withDensity fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞)).withDensity g

Tactic:
ext a : 1
-- Module: Mathlib.Probability.Kernel.WithDensity
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)
h₁ : Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞) * g a x)
⊢ 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:
rw [Kernel.withDensity_apply]

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
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞) * g a x)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.WithDensity
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 (α := 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)
⊢ 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:
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

Premises used: MeasureTheory.Measure.withDensity, ENNReal.ofNNReal, HMul.hMul, ProbabilityTheory.Kernel.withDensity, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.WithDensity
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 (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)
h₁ : Measurable (β := ℝ≥0∞) fun (x : β) ↦ (↑(f a x) : ℝ≥0∞)
h₂ : Measurable (β := ℝ≥0∞) fun (x : β) ↦ g a x
⊢ 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:
rw [withDensity_mul]

Premises used: ProbabilityTheory.Kernel.withDensity_mul
-- Module: Mathlib.Probability.Kernel.WithDensity
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 : Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞))
⊢ 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 [Kernel.withDensity_apply _ hg, Kernel.withDensity_apply]

Premises used: ProbabilityTheory.Kernel.withDensity_apply