awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
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∞)
    ((((κ.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∞)
have h : ∫⁻ (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 [sum_apply' _ a hs, Kernel.withDensity_apply' κ _ a s]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
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
⊢ 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∞)
have rw : Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry (∑' (n : ι), f n))
Tactic: rw [sum_apply' _ a hs, Kernel.withDensity_apply' κ _ a s]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
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))
have h : ∀ (p : α × β), Eq (α := ℝ≥0∞) (Function.uncurry (∑' (n : ι), f n) p) ((∑' (n : ι), Function.uncurry (f n)) p)
Tactic: ext1 p
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
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 : α × β
⊢ Eq (α := ℝ≥0∞) (Function.uncurry (∑' (n : ι), f n) p) ((∑' (n : ι), Function.uncurry (f n)) p)
have h : Eq (α := ℝ≥0∞) ((∑' (n : ι), f n) p.1 p.2) ((∑' (n : ι), fun (p : α × β) ↦ f n p.1 p.2) p)
Tactic: simp only [Function.uncurry_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
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 : α × β
⊢ Eq (α := ℝ≥0∞) ((∑' (n : ι), f n) p.1 p.2) ((∑' (n : ι), fun (p : α × β) ↦ f n p.1 p.2) p)
have h : Summable (α := (x : α × β) → ℝ≥0∞) fun (n : ι) (p : α × β) ↦ f n p.1 p.2
Tactic: rw [tsum_apply h_sum, tsum_apply (h_sum_a _), tsum_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (hypothesis)
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
⊢ Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry (∑' (n : ι), f n))
have this : 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
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∞) (Function.uncurry (∑' (n : ι), f n))
have rw : Measurable (α := α × β) (β := ℝ≥0∞) (∑' (n : ι), Function.uncurry (f n))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
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
have e_f : ∀ (b : β), Eq (α := ℝ≥0∞) ((∑' (n : ι), f n) a b) (∑' (n : ι), (fun (b : β) ↦ f n a b) b)
Tactic: congr with b
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
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 : β
⊢ Eq (α := ℝ≥0∞) ((∑' (n : ι), f n) a b) (∑' (n : ι), (fun (b : β) ↦ f n a b) b)
have e_f : Eq (α := ℝ≥0∞) ((∑' (i : ι), f i a) b) (∑' (n : ι), (fun (b : β) ↦ f n a b) b)
Tactic: rw [tsum_apply h_sum, tsum_apply (h_sum_a a)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
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)
⊢ Eq (α := ℝ≥0∞) ((∑' (n : ι), f n) a b) (∑' (n : ι), (fun (b : β) ↦ f n a b) b)
have e_f₁ : Eq (α := ℝ≥0∞) (∑' (i : ι), f i a b) (∑' (n : ι), (fun (b : β) ↦ f n a b) b)
Tactic: rw [tsum_apply h_sum, tsum_apply (h_sum_a a)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (hypothesis)
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 =
    ∑' (n : ι), (((κ.withDensity (f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
have 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
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)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
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
⊢ ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂(κ : (a : α) → Measure β) a =
    ∑' (n : ι), (((κ.withDensity (f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
have 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)
Tactic: rw [this, lintegral_tsum fun n => by fun_prop]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
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
⊢ 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)
have 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
Tactic: congr with n
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
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 : ι
⊢ ∫⁻ (a_1 : β) in s, f n a a_1 ∂(κ : (a : α) → Measure β) a =
    (((κ.withDensity (f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
have h : ∫⁻ (a_1 : β) in s, f n a a_1 ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β) in s, f n a b ∂(κ : (a : α) → Measure β) a
Tactic: rw [Kernel.withDensity_apply' _ (hf n) a s]
-- 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 κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
⊢ IsFiniteKernel (κ.withDensity f)
have pos : ∀ (hf : Measurable (Function.uncurry f)), IsFiniteKernel (κ.withDensity f)
Tactic: by_cases hf : Measurable (Function.uncurry f)
-- 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 κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
pos : ∀ (hf : Measurable (Function.uncurry f)), IsFiniteKernel (κ.withDensity f)
⊢ IsFiniteKernel (κ.withDensity f)
have neg : ∀ (hf : ¬Measurable (Function.uncurry f)), IsFiniteKernel (κ.withDensity f)
Tactic: by_cases hf : Measurable (Function.uncurry f)
-- 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 κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
a : α
⊢ (((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ B * κ.bound
have rw : ∫⁻ (b : β) in Set.univ, f a b ∂(κ : (a : α) → Measure β) a ≤ B * κ.bound
Tactic: rw [Kernel.withDensity_apply' κ hf a Set.univ]
-- 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 κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
a : α
⊢ HMul.hMul (β := ℝ≥0∞) B ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    B * κ.bound
have grw : B * κ.bound ≤ B * κ.bound
Tactic: grw [measure_le_bound]
-- 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 κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
a : α
⊢ ∫⁻ (b : β) in Set.univ, f a b ∂(κ : (a : α) → Measure β) a ≤ B * κ.bound
have b : ∫⁻ (x : β) in Set.univ, B ∂(κ : (a : α) → Measure β) a =
  HMul.hMul (β := ℝ≥0∞) B ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: calc
          ∫⁻ b in Set.univ, f a b ∂κ a ≤ ∫⁻ _ in Set.univ, B ∂κ a := lintegral_mono (hf_B a)
          _ = B * κ a Set.univ := by
            simp only [Measure.restrict_univ, MeasureTheory.lintegral_const]
          _ ≤ B * κ.bound := by grw [measure_le_bound]
-- 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 κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
a : α
b :
  ∫⁻ (x : β) in Set.univ, B ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (β := ℝ≥0∞) B ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ ∫⁻ (b : β) in Set.univ, f a b ∂(κ : (a : α) → Measure β) a ≤ B * κ.bound
have b₁ : HMul.hMul (β := ℝ≥0∞) B ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ B * κ.bound
Tactic: calc
          ∫⁻ b in Set.univ, f a b ∂κ a ≤ ∫⁻ _ in Set.univ, B ∂κ a := lintegral_mono (hf_B a)
          _ = B * κ a Set.univ := by
            simp only [Measure.restrict_univ, MeasureTheory.lintegral_const]
          _ ≤ B * κ.bound := by grw [measure_le_bound]
-- 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 κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : ¬Measurable (Function.uncurry f)
⊢ IsFiniteKernel (κ.withDensity f)
have neg : IsFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
Tactic: rw [withDensity_of_not_measurable _ hf]
-- 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 ≠ ∞
⊢ IsSFiniteKernel (κ.withDensity f)
have pos : ∀ (hf : Measurable (Function.uncurry f)), IsSFiniteKernel (κ.withDensity f)
Tactic: by_cases hf : Measurable (Function.uncurry f)
-- 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 ≠ ∞
pos : ∀ (hf : Measurable (Function.uncurry f)), IsSFiniteKernel (κ.withDensity f)
⊢ IsSFiniteKernel (κ.withDensity f)
have neg : ∀ (hf : ¬Measurable (Function.uncurry f)), IsSFiniteKernel (κ.withDensity f)
Tactic: by_cases hf : Measurable (Function.uncurry f)
-- 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)
⊢ IsSFiniteKernel (κ.withDensity f)
have neg : IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
Tactic: rw [withDensity_of_not_measurable _ hf]
-- 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∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
⊢ f a b ≤ (↑n : ℝ≥0∞)
have this : (f a b).toReal ≤ (↑n : ℝ)
Tactic: have : (f a b).toReal ≤ n := Nat.le_of_ceil_le 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∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : (f a b).toReal ≤ (↑n : ℝ)
⊢ f a b ≤ (↑n : ℝ≥0∞)
have rw : ∀ (this : f a b ≤ ENNReal.ofReal (↑n : ℝ)), f a b ≤ (↑n : ℝ≥0∞)
Tactic: rw [← ENNReal.le_ofReal_iff_toReal_le (hf_ne_top a b) _] at this
Cleared hypotheses: this
-- 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∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : (f a b).toReal ≤ (↑n : ℝ)
rw : ∀ (this : f a b ≤ ENNReal.ofReal (↑n : ℝ)), f a b ≤ (↑n : ℝ≥0∞)
⊢ f a b ≤ (↑n : ℝ≥0∞)
have rw₁ : LE.le (α := ℝ) 0 (↑n : ℝ)
Tactic: rw [← ENNReal.le_ofReal_iff_toReal_le (hf_ne_top a b) _] at this
-- 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∞)
⊢ IsSFiniteKernel (κ.withDensity f)
have h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
Tactic: have h_le : ∀ a b n, ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ n := by
    intro a b n hn
    have : (f a b).toReal ≤ n := Nat.le_of_ceil_le hn
    rw [← ENNReal.le_ofReal_iff_toReal_le (hf_ne_top a b) _] at this
    · simpa
    · exact n.cast_nonneg
-- 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∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) = f a b ∧ min (f a b) (↑n : ℝ≥0∞) = f a b
simp_rw : min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞) = 0
⊢ fs n a b = 0
have simp_rw₁ : f a b - min (f a b) (↑n : ℝ≥0∞) = 0
Tactic: simp_rw [fs, this.1, this.2, tsub_self (f 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∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) = f a b ∧ min (f a b) (↑n : ℝ≥0∞) = f a b
simp_rw : min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞) = 0
simp_rw₁ : f a b - min (f a b) (↑n : ℝ≥0∞) = 0
⊢ fs n a b = 0
have simp_rw₂ : f a b - f a b = 0
Tactic: simp_rw [fs, this.1, this.2, tsub_self (f 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∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
⊢ fs n a b = 0
have suffices : min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) = f a b ∧ min (f a b) (↑n : ℝ≥0∞) = f a b
Tactic: suffices min (f a b) (n + 1) = f a b ∧ min (f a b) n = f a b by
      simp_rw [fs, this.1, this.2, tsub_self (f a b)]
-- 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∞)
⊢ IsSFiniteKernel (κ.withDensity f)
have h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
Tactic: have h_zero : ∀ a b n, ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0 := by
    intro a b n hn
    suffices min (f a b) (n + 1) = f a b ∧ min (f a b) n = f a b by
      simp_rw [fs, this.1, this.2, tsub_self (f a b)]
    exact ⟨min_eq_left ((h_le a b n hn).trans (le_add_of_nonneg_right zero_le_one)),
      min_eq_left (h_le a b n hn)⟩