[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
⊢ (fun a => Measure.withDensity (↑κ a) (f a)) ∈ kernel α β
[PROOFSTEP]
refine' Measure.measurable_of_measurable_coe _ fun s hs => _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(Measure.withDensity (↑κ b) (f b)) s
[PROOFSTEP]
simp_rw [withDensity_apply _ hs]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ∫⁻ (a : β) in s, f b a ∂↑κ b
[PROOFSTEP]
exact hf.set_lintegral_kernel_prod_right hs
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : ¬Measurable (Function.uncurry f)
⊢ withDensity κ f = 0
[PROOFSTEP]
classical exact dif_neg hf
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : ¬Measurable (Function.uncurry f)
⊢ withDensity κ f = 0
[PROOFSTEP]
exact dif_neg hf
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
⊢ ↑(withDensity κ f) a = Measure.withDensity (↑κ a) (f a)
[PROOFSTEP]
classical
rw [withDensity, dif_pos hf]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
⊢ ↑(withDensity κ f) a = Measure.withDensity (↑κ a) (f a)
[PROOFSTEP]
rw [withDensity, dif_pos hf]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
⊢ ↑{ val := fun a => Measure.withDensity (↑κ a) (f a),
          property := (_ : Measurable fun a => Measure.withDensity (↑κ a) (f a)) }
      a =
    Measure.withDensity (↑κ a) (f a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(withDensity κ f) a) s = ∫⁻ (b : β) in s, f a b ∂↑κ a
[PROOFSTEP]
rw [kernel.withDensity_apply κ hf, withDensity_apply _ hs]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
g : β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (b : β), g b ∂↑(withDensity κ f) a = ∫⁻ (b : β), f a b * g b ∂↑κ a
[PROOFSTEP]
rw [kernel.withDensity_apply _ hf, lintegral_withDensity_eq_lintegral_mul _ (Measurable.of_uncurry_left hf) hg]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
g : β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (a_1 : β), (f a * g) a_1 ∂↑κ a = ∫⁻ (b : β), f a b * g b ∂↑κ a
[PROOFSTEP]
simp_rw [Pi.mul_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ ∫ (b : β), f b ∂↑(withDensity κ fun a b => ↑(g a b)) a = ∫ (b : β), g a b • f b ∂↑κ a
[PROOFSTEP]
rw [kernel.withDensity_apply, integral_withDensity_eq_integral_smul]
[GOAL]
case f_meas
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ Measurable fun b => g a b
[PROOFSTEP]
exact Measurable.of_uncurry_left hg
[GOAL]
case hf
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ Measurable (Function.uncurry fun a b => ↑(g a b))
[PROOFSTEP]
exact measurable_coe_nnreal_ennreal.comp hg
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
κ η : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
⊢ withDensity (κ + η) f = withDensity κ f + withDensity η f
[PROOFSTEP]
by_cases hf : Measurable (Function.uncurry f)
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
κ η : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
⊢ withDensity (κ + η) f = withDensity κ f + withDensity η f
[PROOFSTEP]
ext a s
[GOAL]
case pos.h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
κ η : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
a : α
s : Set β
a✝ : MeasurableSet s
⊢ ↑↑(↑(withDensity (κ + η) f) a) s = ↑↑(↑(withDensity κ f + withDensity η f) a) s
[PROOFSTEP]
simp only [kernel.withDensity_apply _ hf, coeFn_add, Pi.add_apply, withDensity_add_measure, Measure.add_apply]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
κ η : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ withDensity (κ + η) f = withDensity κ f + withDensity η f
[PROOFSTEP]
simp_rw [withDensity_of_not_measurable _ hf]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
κ η : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ 0 = 0 + 0
[PROOFSTEP]
rw [zero_add]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝ : Countable ι
κ : ι → { x // x ∈ kernel α β }
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
⊢ withDensity (kernel.sum κ) f = kernel.sum fun i => withDensity (κ i) f
[PROOFSTEP]
by_cases hf : Measurable (Function.uncurry f)
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝ : Countable ι
κ : ι → { x // x ∈ kernel α β }
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
⊢ withDensity (kernel.sum κ) f = kernel.sum fun i => withDensity (κ i) f
[PROOFSTEP]
ext1 a
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝ : Countable ι
κ : ι → { x // x ∈ kernel α β }
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
a : α
⊢ ↑(withDensity (kernel.sum κ) f) a = ↑(kernel.sum fun i => withDensity (κ i) f) a
[PROOFSTEP]
simp_rw [sum_apply, kernel.withDensity_apply _ hf, sum_apply, withDensity_sum (fun n => κ n a) (f a)]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝ : Countable ι
κ : ι → { x // x ∈ kernel α β }
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ withDensity (kernel.sum κ) f = kernel.sum fun i => withDensity (κ i) f
[PROOFSTEP]
simp_rw [withDensity_of_not_measurable _ hf]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝ : Countable ι
κ : ι → { x // x ∈ kernel α β }
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ 0 = kernel.sum fun i => 0
[PROOFSTEP]
exact sum_zero.symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
⊢ withDensity κ (∑' (n : ι), f n) = kernel.sum fun n => withDensity κ (f n)
[PROOFSTEP]
have h_sum_a : ∀ a, Summable fun n => f n a := fun a => Pi.summable.mpr fun b => ENNReal.summable
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
⊢ withDensity κ (∑' (n : ι), f n) = kernel.sum fun n => withDensity κ (f n)
[PROOFSTEP]
have h_sum : Summable fun n => f n := Pi.summable.mpr h_sum_a
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
⊢ withDensity κ (∑' (n : ι), f n) = kernel.sum fun n => withDensity κ (f n)
[PROOFSTEP]
ext a s hs
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(withDensity κ (∑' (n : ι), f n)) a) s = ↑↑(↑(kernel.sum fun n => withDensity κ (f n)) a) s
[PROOFSTEP]
rw [sum_apply' _ a hs, withDensity_apply' κ _ a hs]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, tsum (fun n => f n) a b ∂↑κ a = ∑' (n : ι), ↑↑(↑(withDensity κ (f n)) a) s
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable (Function.uncurry (∑' (n : ι), f n))
[PROOFSTEP]
swap
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable (Function.uncurry (∑' (n : ι), f n))
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
⊢ Function.uncurry (∑' (n : ι), f n) = ∑' (n : ι), Function.uncurry (f n)
[PROOFSTEP]
ext1 p
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
⊢ Function.uncurry (∑' (n : ι), f n) p = tsum (fun n => Function.uncurry (f n)) p
[PROOFSTEP]
simp only [Function.uncurry_def]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
⊢ tsum (fun n => f n) p.fst p.snd = tsum (fun n p => f n p.fst p.snd) p
[PROOFSTEP]
rw [tsum_apply h_sum, tsum_apply (h_sum_a _), tsum_apply]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
⊢ Summable fun n p => f n p.fst p.snd
[PROOFSTEP]
exact Pi.summable.mpr fun p => ENNReal.summable
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
this : Function.uncurry (∑' (n : ι), f n) = ∑' (n : ι), Function.uncurry (f n)
⊢ Measurable (Function.uncurry (∑' (n : ι), f n))
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
this : Function.uncurry (∑' (n : ι), f n) = ∑' (n : ι), Function.uncurry (f n)
⊢ Measurable (∑' (n : ι), Function.uncurry (f n))
[PROOFSTEP]
exact Measurable.ennreal_tsum' hf
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, tsum (fun n => f n) a b ∂↑κ a = ∑' (n : ι), ↑↑(↑(withDensity κ (f n)) a) s
[PROOFSTEP]
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)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, tsum (fun n => f n) a b ∂↑κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂↑κ a
[PROOFSTEP]
congr with b
[GOAL]
case e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
b : β
⊢ tsum (fun n => f n) a b = ∑' (n : ι), (fun b => f n a b) b
[PROOFSTEP]
rw [tsum_apply h_sum, tsum_apply (h_sum_a a)]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
this : ∫⁻ (b : β) in s, tsum (fun n => f n) a b ∂↑κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂↑κ a
⊢ ∫⁻ (b : β) in s, tsum (fun n => f n) a b ∂↑κ a = ∑' (n : ι), ↑↑(↑(withDensity κ (f n)) a) s
[PROOFSTEP]
rw [this, lintegral_tsum fun n => (Measurable.of_uncurry_left (hf n)).aemeasurable]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
this : ∫⁻ (b : β) in s, tsum (fun n => f n) a b ∂↑κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂↑κ a
⊢ ∑' (i : ι), ∫⁻ (a_1 : β) in s, f i a a_1 ∂↑κ a = ∑' (n : ι), ↑↑(↑(withDensity κ (f n)) a) s
[PROOFSTEP]
congr with n
[GOAL]
case h.h.e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f✝ : α → β → ℝ≥0∞
inst✝¹ : Countable ι
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
this : ∫⁻ (b : β) in s, tsum (fun n => f n) a b ∂↑κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂↑κ a
n : ι
⊢ ∫⁻ (a_1 : β) in s, f n a a_1 ∂↑κ a = ↑↑(↑(withDensity κ (f n)) a) s
[PROOFSTEP]
rw [withDensity_apply' _ (hf n) a hs]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ⊤
hf_B : ∀ (a : α) (b : β), f a b ≤ B
⊢ IsFiniteKernel (withDensity κ f)
[PROOFSTEP]
by_cases hf : Measurable (Function.uncurry f)
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ⊤
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
⊢ IsFiniteKernel (withDensity κ f)
[PROOFSTEP]
exact
  ⟨⟨B * IsFiniteKernel.bound κ, ENNReal.mul_lt_top hB_top (IsFiniteKernel.bound_ne_top κ), fun a =>
      by
      rw [withDensity_apply' κ hf a MeasurableSet.univ]
      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 * IsFiniteKernel.bound κ := mul_le_mul_left' (measure_le_bound κ a Set.univ) _⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) Set.univ ≤ B * IsFiniteKernel.bound κ
[PROOFSTEP]
rw [withDensity_apply' κ hf a MeasurableSet.univ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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 ≤ B * IsFiniteKernel.bound κ
[PROOFSTEP]
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 * IsFiniteKernel.bound κ := mul_le_mul_left' (measure_le_bound κ a Set.univ) _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ⊤
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
a : α
⊢ ∫⁻ (x : β) in Set.univ, B ∂↑κ a = B * ↑↑(↑κ a) Set.univ
[PROOFSTEP]
simp only [Measure.restrict_univ, MeasureTheory.lintegral_const]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ⊤
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : ¬Measurable (Function.uncurry f)
⊢ IsFiniteKernel (withDensity κ f)
[PROOFSTEP]
rw [withDensity_of_not_measurable _ hf]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ⊤
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : ¬Measurable (Function.uncurry f)
⊢ IsFiniteKernel 0
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
⊢ IsSFiniteKernel (withDensity κ f)
[PROOFSTEP]
by_cases hf : Measurable (Function.uncurry f)
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
hf : Measurable (Function.uncurry f)
⊢ IsSFiniteKernel (withDensity κ f)
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
hf : ¬Measurable (Function.uncurry f)
⊢ IsSFiniteKernel (withDensity κ f)
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
hf : ¬Measurable (Function.uncurry f)
⊢ IsSFiniteKernel (withDensity κ f)
[PROOFSTEP]
rw [withDensity_of_not_measurable _ hf]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
hf : ¬Measurable (Function.uncurry f)
⊢ IsSFiniteKernel 0
[PROOFSTEP]
infer_instance
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
hf : Measurable (Function.uncurry f)
⊢ IsSFiniteKernel (withDensity κ f)
[PROOFSTEP]
let fs : ℕ → α → β → ℝ≥0∞ := fun n a b => min (f a b) (n + 1) - min (f a b) n
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
⊢ IsSFiniteKernel (withDensity κ f)
[PROOFSTEP]
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 
  · refine' this.trans (le_of_eq _)
    rw [ENNReal.ofReal_coe_nat]
  · norm_cast
    exact zero_le _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
⊢ ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
[PROOFSTEP]
intro a b n hn
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
a : α
b : β
n : ℕ
hn : ⌈ENNReal.toReal (f a b)⌉₊ ≤ n
⊢ f a b ≤ ↑n
[PROOFSTEP]
have : (f a b).toReal ≤ n := Nat.le_of_ceil_le hn
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
a : α
b : β
n : ℕ
hn : ⌈ENNReal.toReal (f a b)⌉₊ ≤ n
this : ENNReal.toReal (f a b) ≤ ↑n
⊢ f a b ≤ ↑n
[PROOFSTEP]
rw [← ENNReal.le_ofReal_iff_toReal_le (hf_ne_top a b) _] at this 
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
a : α
b : β
n : ℕ
hn : ⌈ENNReal.toReal (f a b)⌉₊ ≤ n
this : f a b ≤ ENNReal.ofReal ↑n
⊢ f a b ≤ ↑n
[PROOFSTEP]
refine' this.trans (le_of_eq _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
a : α
b : β
n : ℕ
hn : ⌈ENNReal.toReal (f a b)⌉₊ ≤ n
this : f a b ≤ ENNReal.ofReal ↑n
⊢ ENNReal.ofReal ↑n = ↑n
[PROOFSTEP]
rw [ENNReal.ofReal_coe_nat]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
a : α
b : β
n : ℕ
hn : ⌈ENNReal.toReal (f a b)⌉₊ ≤ n
this : ENNReal.toReal (f a b) ≤ ↑n
⊢ 0 ≤ ↑n
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
a : α
b : β
n : ℕ
hn : ⌈ENNReal.toReal (f a b)⌉₊ ≤ n
this : ENNReal.toReal (f a b) ≤ ↑n
⊢ 0 ≤ n
[PROOFSTEP]
exact zero_le _
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
⊢ IsSFiniteKernel (withDensity κ f)
[PROOFSTEP]
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 [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)⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
⊢ ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
[PROOFSTEP]
intro a b n hn
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
a : α
b : β
n : ℕ
hn : ⌈ENNReal.toReal (f a b)⌉₊ ≤ n
⊢ fs n a b = 0
[PROOFSTEP]
suffices min (f a b) (n + 1) = f a b ∧ min (f a b) n = f a b by simp_rw [this.1, this.2, tsub_self (f a b)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
a : α
b : β
n : ℕ
hn : ⌈ENNReal.toReal (f a b)⌉₊ ≤ n
this : min (f a b) (↑n + 1) = f a b ∧ min (f a b) ↑n = f a b
⊢ fs n a b = 0
[PROOFSTEP]
simp_rw [this.1, this.2, tsub_self (f a b)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
a : α
b : β
n : ℕ
hn : ⌈ENNReal.toReal (f a b)⌉₊ ≤ n
⊢ min (f a b) (↑n + 1) = f a b ∧ min (f a b) ↑n = f a b
[PROOFSTEP]
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)⟩
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
⊢ IsSFiniteKernel (withDensity κ f)
[PROOFSTEP]
have hf_eq_tsum : f = ∑' n, fs n :=
  by
  have h_sum_a : ∀ a, Summable fun n => fs n a :=
    by
    refine' fun a => Pi.summable.mpr fun b => _
    suffices : ∀ n, n ∉ Finset.range ⌈(f a b).toReal⌉₊ → fs n a b = 0
    exact summable_of_ne_finset_zero this
    intro n hn_not_mem
    rw [Finset.mem_range, not_lt] at hn_not_mem 
    exact h_zero a b n hn_not_mem
  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_finset_sum : ∀ n, ∑ i in Finset.range n, fs i a b = min (f a b) n :=
    by
    intro n
    induction' n with n hn
    · simp
    rw [Finset.sum_range_succ, hn]
    simp
  simp_rw [h_finset_sum]
  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⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
⊢ f = ∑' (n : ℕ), fs n
[PROOFSTEP]
have h_sum_a : ∀ a, Summable fun n => fs n a :=
  by
  refine' fun a => Pi.summable.mpr fun b => _
  suffices : ∀ n, n ∉ Finset.range ⌈(f a b).toReal⌉₊ → fs n a b = 0
  exact summable_of_ne_finset_zero this
  intro n hn_not_mem
  rw [Finset.mem_range, not_lt] at hn_not_mem 
  exact h_zero a b n hn_not_mem
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
⊢ ∀ (a : α), Summable fun n => fs n a
[PROOFSTEP]
refine' fun a => Pi.summable.mpr fun b => _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
a : α
b : β
⊢ Summable fun i => fs i a b
[PROOFSTEP]
suffices : ∀ n, n ∉ Finset.range ⌈(f a b).toReal⌉₊ → fs n a b = 0
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
a : α
b : β
this : ∀ (n : ℕ), ¬n ∈ Finset.range ⌈ENNReal.toReal (f a b)⌉₊ → fs n a b = 0
⊢ Summable fun i => fs i a b
case this
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
a : α
b : β
⊢ ∀ (n : ℕ), ¬n ∈ Finset.range ⌈ENNReal.toReal (f a b)⌉₊ → fs n a b = 0
[PROOFSTEP]
exact summable_of_ne_finset_zero this
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
a : α
b : β
⊢ ∀ (n : ℕ), ¬n ∈ Finset.range ⌈ENNReal.toReal (f a b)⌉₊ → fs n a b = 0
[PROOFSTEP]
intro n hn_not_mem
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
a : α
b : β
n : ℕ
hn_not_mem : ¬n ∈ Finset.range ⌈ENNReal.toReal (f a b)⌉₊
⊢ fs n a b = 0
[PROOFSTEP]
rw [Finset.mem_range, not_lt] at hn_not_mem 
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
a : α
b : β
n : ℕ
hn_not_mem : ⌈ENNReal.toReal (f a b)⌉₊ ≤ n
⊢ fs n a b = 0
[PROOFSTEP]
exact h_zero a b n hn_not_mem
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n => fs n a
⊢ f = ∑' (n : ℕ), fs n
[PROOFSTEP]
ext a b : 2
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n => fs n a
a : α
b : β
⊢ f a b = tsum (fun n => fs n) a b
[PROOFSTEP]
rw [tsum_apply (Pi.summable.mpr h_sum_a), tsum_apply (h_sum_a a), ENNReal.tsum_eq_liminf_sum_nat]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n => fs n a
a : α
b : β
⊢ f a b = Filter.liminf (fun n => ∑ i in Finset.range n, fs i a b) Filter.atTop
[PROOFSTEP]
have h_finset_sum : ∀ n, ∑ i in Finset.range n, fs i a b = min (f a b) n :=
  by
  intro n
  induction' n with n hn
  · simp
  rw [Finset.sum_range_succ, hn]
  simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n => fs n a
a : α
b : β
⊢ ∀ (n : ℕ), ∑ i in Finset.range n, fs i a b = min (f a b) ↑n
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n => fs n a
a : α
b : β
n : ℕ
⊢ ∑ i in Finset.range n, fs i a b = min (f a b) ↑n
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n => fs n a
a : α
b : β
⊢ ∑ i in Finset.range Nat.zero, fs i a b = min (f a b) ↑Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n => fs n a
a : α
b : β
n : ℕ
hn : ∑ i in Finset.range n, fs i a b = min (f a b) ↑n
⊢ ∑ i in Finset.range (Nat.succ n), fs i a b = min (f a b) ↑(Nat.succ n)
[PROOFSTEP]
rw [Finset.sum_range_succ, hn]
[GOAL]
case succ
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n => fs n a
a : α
b : β
n : ℕ
hn : ∑ i in Finset.range n, fs i a b = min (f a b) ↑n
⊢ min (f a b) ↑n + fs n a b = min (f a b) ↑(Nat.succ n)
[PROOFSTEP]
simp
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n => fs n a
a : α
b : β
h_finset_sum : ∀ (n : ℕ), ∑ i in Finset.range n, fs i a b = min (f a b) ↑n
⊢ f a b = Filter.liminf (fun n => ∑ i in Finset.range n, fs i a b) Filter.atTop
[PROOFSTEP]
simp_rw [h_finset_sum]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n => fs n a
a : α
b : β
h_finset_sum : ∀ (n : ℕ), ∑ i in Finset.range n, fs i a b = min (f a b) ↑n
⊢ f a b = Filter.liminf (fun n => min (f a b) ↑n) Filter.atTop
[PROOFSTEP]
refine' (Filter.Tendsto.liminf_eq _).symm
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n => fs n a
a : α
b : β
h_finset_sum : ∀ (n : ℕ), ∑ i in Finset.range n, fs i a b = min (f a b) ↑n
⊢ Filter.Tendsto (fun n => min (f a b) ↑n) Filter.atTop (nhds (f a b))
[PROOFSTEP]
refine' Filter.Tendsto.congr' _ tendsto_const_nhds
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n => fs n a
a : α
b : β
h_finset_sum : ∀ (n : ℕ), ∑ i in Finset.range n, fs i a b = min (f a b) ↑n
⊢ (fun x => f a b) =ᶠ[Filter.atTop] fun n => min (f a b) ↑n
[PROOFSTEP]
rw [Filter.EventuallyEq, Filter.eventually_atTop]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n => fs n a
a : α
b : β
h_finset_sum : ∀ (n : ℕ), ∑ i in Finset.range n, fs i a b = min (f a b) ↑n
⊢ ∃ a_1, ∀ (b_1 : ℕ), b_1 ≥ a_1 → f a b = min (f a b) ↑b_1
[PROOFSTEP]
exact ⟨⌈(f a b).toReal⌉₊, fun n hn => (min_eq_left (h_le a b n hn)).symm⟩
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
⊢ IsSFiniteKernel (withDensity κ f)
[PROOFSTEP]
rw [hf_eq_tsum, withDensity_tsum _ fun n : ℕ => _]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
⊢ IsSFiniteKernel (kernel.sum fun n => withDensity κ (fs n))
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
⊢ ∀ (n : ℕ), Measurable (Function.uncurry (fs n))
[PROOFSTEP]
swap
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
⊢ ∀ (n : ℕ), Measurable (Function.uncurry (fs n))
[PROOFSTEP]
exact fun _ => (hf.min measurable_const).sub (hf.min measurable_const)
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
⊢ IsSFiniteKernel (kernel.sum fun n => withDensity κ (fs n))
[PROOFSTEP]
refine' isSFiniteKernel_sum fun n => _
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
⊢ IsSFiniteKernel (withDensity κ (fs n))
[PROOFSTEP]
suffices IsFiniteKernel (withDensity κ (fs n)) by haveI := this; infer_instance
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
this : IsFiniteKernel (withDensity κ (fs n))
⊢ IsSFiniteKernel (withDensity κ (fs n))
[PROOFSTEP]
haveI := this
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
this✝ this : IsFiniteKernel (withDensity κ (fs n))
⊢ IsSFiniteKernel (withDensity κ (fs n))
[PROOFSTEP]
infer_instance
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
⊢ IsFiniteKernel (withDensity κ (fs n))
[PROOFSTEP]
refine' isFiniteKernel_withDensity_of_bounded _ (ENNReal.coe_ne_top : ↑n + 1 ≠ ∞) fun a b => _
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
a : α
b : β
⊢ fs n a b ≤ ↑((fun x x_1 => x + x_1) (↑n) 1)
[PROOFSTEP]
norm_cast
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
a : α
b : β
⊢ fs n a b ≤ ↑(n + 1)
[PROOFSTEP]
calc
  fs n a b ≤ min (f a b) (n + 1) := tsub_le_self
  _ ≤ n + 1 := (min_le_right _ _)
  _ = ↑(n + 1) := by norm_cast
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ 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) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈ENNReal.toReal (f a b)⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
a : α
b : β
⊢ ↑n + 1 = ↑(n + 1)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
⊢ IsSFiniteKernel (kernel.withDensity κ f)
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
⊢ kernel.withDensity κ f = kernel.sum fun i => kernel.withDensity (seq κ i) f
[PROOFSTEP]
rw [← withDensity_kernel_sum _ _]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
⊢ kernel.withDensity κ f = kernel.withDensity (kernel.sum fun i => seq κ i) f
[PROOFSTEP]
congr
[GOAL]
case e_κ
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
⊢ κ = kernel.sum fun i => seq κ i
[PROOFSTEP]
exact (kernel_sum_seq κ).symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
h_eq_sum : kernel.withDensity κ f = kernel.sum fun i => kernel.withDensity (seq κ i) f
⊢ IsSFiniteKernel (kernel.withDensity κ f)
[PROOFSTEP]
rw [h_eq_sum]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
f : α → β → ℝ≥0∞
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
h_eq_sum : kernel.withDensity κ f = kernel.sum fun i => kernel.withDensity (seq κ i) f
⊢ IsSFiniteKernel (kernel.sum fun i => kernel.withDensity (seq κ i) f)
[PROOFSTEP]
exact isSFiniteKernel_sum fun n => isSFiniteKernel_withDensity_of_isFiniteKernel (seq κ n) hf_ne_top
