[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


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
⊢ ↑p a = 0 ↔ ¬a ∈ support p
[PROOFSTEP]
rw [mem_support_iff, Classical.not_not]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
⊢ ↑p a = 1 ↔ support p = {a}
[PROOFSTEP]
refine'
  ⟨fun h =>
    Set.Subset.antisymm (fun a' ha' => by_contra fun ha => _) fun a' ha' =>
      ha'.symm ▸ (p.mem_support_iff a).2 fun ha => zero_ne_one <| ha.symm.trans h,
    fun h => _root_.trans (symm <| tsum_eq_single a fun a' ha' => (p.apply_eq_zero_iff a').2 (h.symm ▸ ha')) p.tsum_coe⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
⊢ False
[PROOFSTEP]
suffices : 1 < ∑' a, p a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 1 < ∑' (a : α), ↑p a
⊢ False
case this
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
⊢ 1 < ∑' (a : α), ↑p a
[PROOFSTEP]
exact ne_of_lt this p.tsum_coe.symm
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
⊢ 1 < ∑' (a : α), ↑p a
[PROOFSTEP]
have : 0 < ∑' b, ite (b = a) 0 (p b) :=
  lt_of_le_of_ne' zero_le'
    ((tsum_ne_zero_iff ENNReal.summable).2 ⟨a', ite_ne_left_iff.2 ⟨ha, Ne.symm <| (p.mem_support_iff a').2 ha'⟩⟩)
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
⊢ 1 < ∑' (a : α), ↑p a
[PROOFSTEP]
calc
  1 = 1 + 0 := (add_zero 1).symm
  _ < p a + ∑' b, ite (b = a) 0 (p b) := (ENNReal.add_lt_add_of_le_of_lt ENNReal.one_ne_top (le_of_eq h.symm) this)
  _ = ite (a = a) (p a) 0 + ∑' b, ite (b = a) 0 (p b) := by rw [eq_self_iff_true, if_true]
  _ = (∑' b, ite (b = a) (p b) 0) + ∑' b, ite (b = a) 0 (p b) :=
    by
    congr
    exact symm (tsum_eq_single a fun b hb => if_neg hb)
  _ = ∑' b, (ite (b = a) (p b) 0 + ite (b = a) 0 (p b)) := ENNReal.tsum_add.symm
  _ = ∑' b, p b := tsum_congr fun b => by split_ifs <;> simp only [zero_add, add_zero, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
⊢ (↑p a + ∑' (b : α), if b = a then 0 else ↑p b) = (if a = a then ↑p a else 0) + ∑' (b : α), if b = a then 0 else ↑p b
[PROOFSTEP]
rw [eq_self_iff_true, if_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
⊢ ((if a = a then ↑p a else 0) + ∑' (b : α), if b = a then 0 else ↑p b) =
    (∑' (b : α), if b = a then ↑p b else 0) + ∑' (b : α), if b = a then 0 else ↑p b
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
⊢ (if a = a then ↑p a else 0) = ∑' (b : α), if b = a then ↑p b else 0
[PROOFSTEP]
exact symm (tsum_eq_single a fun b hb => if_neg hb)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
b : α
⊢ ((if b = a then ↑p b else 0) + if b = a then 0 else ↑p b) = ↑p b
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
b : α
h✝ : b = a
⊢ ↑p b + 0 = ↑p b
[PROOFSTEP]
simp only [zero_add, add_zero, le_rfl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
b : α
h✝ : ¬b = a
⊢ 0 + ↑p b = ↑p b
[PROOFSTEP]
simp only [zero_add, add_zero, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
⊢ ↑p a ≤ 1
[PROOFSTEP]
refine' hasSum_le (fun b => _) (hasSum_ite_eq a (p a)) (hasSum_coe_one p)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a b : α
⊢ (if b = a then ↑p a else 0) ≤ ↑p b
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a b : α
h : b = a
⊢ ↑p a ≤ ↑p b
[PROOFSTEP]
simp only [h, zero_le', le_rfl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a b : α
h : ¬b = a
⊢ 0 ≤ ↑p b
[PROOFSTEP]
simp only [h, zero_le', le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
⊢ OuterMeasure.caratheodory (toOuterMeasure p) = ⊤
[PROOFSTEP]
refine' eq_top_iff.2 <| le_trans (le_sInf fun x hx => _) (le_sum_caratheodory _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
x : MeasurableSpace α
hx : x ∈ Set.range fun i => OuterMeasure.caratheodory (↑p i • dirac i)
⊢ ⊤ ≤ x
[PROOFSTEP]
have ⟨y, hy⟩ := hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
x : MeasurableSpace α
hx : x ∈ Set.range fun i => OuterMeasure.caratheodory (↑p i • dirac i)
y : α
hy : (fun i => OuterMeasure.caratheodory (↑p i • dirac i)) y = x
⊢ ⊤ ≤ x
[PROOFSTEP]
exact ((le_of_eq (dirac_caratheodory y).symm).trans (le_smul_caratheodory _ _)).trans (le_of_eq hy)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s✝ t : Set α
s : Finset α
⊢ ↑(toOuterMeasure p) ↑s = ∑ x in s, ↑p x
[PROOFSTEP]
refine' (toOuterMeasure_apply p s).trans ((tsum_eq_sum (s := s) _).trans _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s✝ t : Set α
s : Finset α
⊢ ∀ (b : α), ¬b ∈ s → Set.indicator (↑s) (↑p) b = 0
[PROOFSTEP]
exact fun x hx => Set.indicator_of_not_mem (Finset.mem_coe.not.2 hx) _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s✝ t : Set α
s : Finset α
⊢ ∑ b in s, Set.indicator (↑s) (↑p) b = ∑ x in s, ↑p x
[PROOFSTEP]
exact Finset.sum_congr rfl fun x hx => Set.indicator_of_mem (Finset.mem_coe.2 hx) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
a : α
⊢ ↑(toOuterMeasure p) {a} = ↑p a
[PROOFSTEP]
refine' (p.toOuterMeasure_apply { a }).trans ((tsum_eq_single a fun b hb => _).trans _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
a b : α
hb : b ≠ a
⊢ Set.indicator {a} (↑p) b = 0
[PROOFSTEP]
exact ite_eq_right_iff.2 fun hb' => False.elim <| hb hb'
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
a : α
⊢ Set.indicator {a} (↑p) a = ↑p a
[PROOFSTEP]
exact ite_eq_left_iff.2 fun ha' => False.elim <| ha' rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
⊢ ↑(toOuterMeasure p) s = 0 ↔ Disjoint (support p) s
[PROOFSTEP]
rw [toOuterMeasure_apply, ENNReal.tsum_eq_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
⊢ (∀ (i : α), Set.indicator s (↑p) i = 0) ↔ Disjoint (support p) s
[PROOFSTEP]
exact Function.funext_iff.symm.trans Set.indicator_eq_zero'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
⊢ ↑(toOuterMeasure p) s = 1 ↔ support p ⊆ s
[PROOFSTEP]
refine' (p.toOuterMeasure_apply s).symm ▸ ⟨fun h a hap => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : ∑' (x : α), Set.indicator s (↑p) x = 1
a : α
hap : a ∈ support p
⊢ a ∈ s
[PROOFSTEP]
refine' by_contra fun hs => ne_of_lt _ (h.trans p.tsum_coe.symm)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : ∑' (x : α), Set.indicator s (↑p) x = 1
a : α
hap : a ∈ support p
hs : ¬a ∈ s
⊢ ∑' (x : α), Set.indicator s (↑p) x < ∑' (a : α), ↑p a
[PROOFSTEP]
have hs' : s.indicator p a = 0 := Set.indicator_apply_eq_zero.2 fun hs' => False.elim <| hs hs'
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : ∑' (x : α), Set.indicator s (↑p) x = 1
a : α
hap : a ∈ support p
hs : ¬a ∈ s
hs' : Set.indicator s (↑p) a = 0
⊢ ∑' (x : α), Set.indicator s (↑p) x < ∑' (a : α), ↑p a
[PROOFSTEP]
have hsa : s.indicator p a < p a := hs'.symm ▸ (p.apply_pos_iff a).2 hap
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : ∑' (x : α), Set.indicator s (↑p) x = 1
a : α
hap : a ∈ support p
hs : ¬a ∈ s
hs' : Set.indicator s (↑p) a = 0
hsa : Set.indicator s (↑p) a < ↑p a
⊢ ∑' (x : α), Set.indicator s (↑p) x < ∑' (a : α), ↑p a
[PROOFSTEP]
exact ENNReal.tsum_lt_tsum (p.tsum_coe_indicator_ne_top s) (fun x => Set.indicator_apply_le fun _ => le_rfl) hsa
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : support p ⊆ s
⊢ ∑' (x : α), Set.indicator s (↑p) x = 1
[PROOFSTEP]
suffices : ∀ (x) (_ : x ∉ s), p x = 0
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : support p ⊆ s
this : ∀ (x : α), ¬x ∈ s → ↑p x = 0
⊢ ∑' (x : α), Set.indicator s (↑p) x = 1
case this α : Type u_1 β : Type u_2 γ : Type u_3 p : Pmf α s t : Set α h : support p ⊆ s ⊢ ∀ (x : α), ¬x ∈ s → ↑p x = 0
[PROOFSTEP]
exact
  _root_.trans (tsum_congr fun a => (Set.indicator_apply s p a).trans (ite_eq_left_iff.2 <| symm ∘ this a)) p.tsum_coe
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : support p ⊆ s
⊢ ∀ (x : α), ¬x ∈ s → ↑p x = 0
[PROOFSTEP]
exact fun a ha => (p.apply_eq_zero_iff a).2 <| Set.not_mem_subset h ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
⊢ ↑(toOuterMeasure p) (s ∩ support p) = ↑(toOuterMeasure p) s
[PROOFSTEP]
simp only [toOuterMeasure_apply, Pmf.support, Set.indicator_inter_support]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
p : Pmf α
s t : Set α
a : α
h : MeasurableSet {a}
⊢ ↑↑(toMeasure p) {a} = ↑p a
[PROOFSTEP]
simp [toMeasure_apply_eq_toOuterMeasure_apply _ _ h, toOuterMeasure_apply_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
p : Pmf α
s t : Set α
hs : MeasurableSet s
⊢ ↑↑(toMeasure p) s = 0 ↔ Disjoint (support p) s
[PROOFSTEP]
rw [toMeasure_apply_eq_toOuterMeasure_apply p s hs, toOuterMeasure_apply_eq_zero_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
p : Pmf α
s t : Set α
hs : MeasurableSet s
hp : MeasurableSet (support p)
⊢ ↑↑(toMeasure p) (s ∩ support p) = ↑↑(toMeasure p) s
[PROOFSTEP]
simp [p.toMeasure_apply_eq_toOuterMeasure_apply s hs, p.toMeasure_apply_eq_toOuterMeasure_apply _ (hs.inter hp)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
p : Pmf α
s✝ t✝ s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : s ∩ support p ⊆ t
⊢ ↑↑(toMeasure p) s ≤ ↑↑(toMeasure p) t
[PROOFSTEP]
simpa only [p.toMeasure_apply_eq_toOuterMeasure_apply, hs, ht] using toOuterMeasure_mono p h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
p : Pmf α
s✝ t✝ s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : s ∩ support p = t ∩ support p
⊢ ↑↑(toMeasure p) s = ↑↑(toMeasure p) t
[PROOFSTEP]
simpa only [p.toMeasure_apply_eq_toOuterMeasure_apply, hs, ht] using toOuterMeasure_apply_eq_of_inter_support_eq p h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : MeasurableSpace α
p : Pmf α
s t : Set α
inst✝ : MeasurableSingletonClass α
⊢ Function.Injective toMeasure
[PROOFSTEP]
intro p q h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : MeasurableSpace α
p✝ : Pmf α
s t : Set α
inst✝ : MeasurableSingletonClass α
p q : Pmf α
h : toMeasure p = toMeasure q
⊢ p = q
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : MeasurableSpace α
p✝ : Pmf α
s t : Set α
inst✝ : MeasurableSingletonClass α
p q : Pmf α
h : toMeasure p = toMeasure q
x : α
⊢ ↑p x = ↑q x
[PROOFSTEP]
rw [← p.toMeasure_apply_singleton x <| measurableSet_singleton x, ←
  q.toMeasure_apply_singleton x <| measurableSet_singleton x, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑(toMeasure (toPmf μ)) s = ↑↑μ s
[PROOFSTEP]
rw [μ.toPmf.toMeasure_apply s hs, ← μ.tsum_indicator_apply_singleton s hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), Set.indicator s (↑(toPmf μ)) x = ∑' (x : α), Set.indicator s (fun x => ↑↑μ {x}) x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
p : Pmf α
⊢ ↑↑(toMeasure p) Set.univ = 1
[PROOFSTEP]
simpa only [MeasurableSet.univ, toMeasure_apply_eq_toOuterMeasure_apply, Set.indicator_univ, toOuterMeasure_apply,
  ENNReal.coe_eq_one] using tsum_coe p
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : Pmf α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
x : α
⊢ ↑(Measure.toPmf (toMeasure p)) x = ↑p x
[PROOFSTEP]
rw [← p.toMeasure_apply_singleton x (measurableSet_singleton x), p.toMeasure.toPmf_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : Countable α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
p : Pmf α
μ✝ : Measure α
inst✝¹ : IsProbabilityMeasure μ✝
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ toMeasure p = μ ↔ p = Measure.toPmf μ
[PROOFSTEP]
rw [← toMeasure_inj, Measure.toPmf_toMeasure]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : Countable α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
p : Pmf α
μ✝ : Measure α
inst✝¹ : IsProbabilityMeasure μ✝
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ Measure.toPmf μ = p ↔ μ = toMeasure p
[PROOFSTEP]
rw [← toMeasure_inj, Measure.toPmf_toMeasure]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
⊢ Pmf α
[PROOFSTEP]
refine' ofFinset (fun a => if a ∈ s then s.card⁻¹ else 0) s _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
⊢ ∑ a in s, (fun a => if a ∈ s then (↑(Finset.card s))⁻¹ else 0) a = 1
[PROOFSTEP]
simp only [Finset.sum_ite_mem, Finset.inter_self, Finset.sum_const, nsmul_eq_mul]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
⊢ ↑(Finset.card s) * (↑(Finset.card s))⁻¹ = 1
[PROOFSTEP]
have : (s.card : ℝ≥0∞) ≠ 0 := by
  simpa only [Ne.def, Nat.cast_eq_zero, Finset.card_eq_zero] using Finset.nonempty_iff_ne_empty.1 hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
⊢ ↑(Finset.card s) ≠ 0
[PROOFSTEP]
simpa only [Ne.def, Nat.cast_eq_zero, Finset.card_eq_zero] using Finset.nonempty_iff_ne_empty.1 hs
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
this : ↑(Finset.card s) ≠ 0
⊢ ↑(Finset.card s) * (↑(Finset.card s))⁻¹ = 1
[PROOFSTEP]
refine' ENNReal.mul_inv_cancel this <| ENNReal.nat_ne_top s.card
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
⊢ ∀ (a : α), ¬a ∈ s → (fun a => if a ∈ s then (↑(Finset.card s))⁻¹ else 0) a = 0
[PROOFSTEP]
exact fun x hx => by simp only [hx, if_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
x : α
hx : ¬x ∈ s
⊢ (fun a => if a ∈ s then (↑(Finset.card s))⁻¹ else 0) x = 0
[PROOFSTEP]
simp only [hx, if_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
ha : a ∈ s
⊢ ↑(uniformOfFinset s hs) a = (↑(Finset.card s))⁻¹
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
ha : ¬a ∈ s
⊢ ↑(uniformOfFinset s hs) a = 0
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
⊢ ∀ (x : α), x ∈ support (uniformOfFinset s hs) ↔ x ∈ ↑s
[PROOFSTEP]
let ⟨a, ha⟩ := hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a✝ a : α
ha : a ∈ s
⊢ ∀ (x : α), x ∈ support (uniformOfFinset s (_ : ∃ x, x ∈ s)) ↔ x ∈ ↑s
[PROOFSTEP]
simp [mem_support_iff, Finset.ne_empty_of_mem ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a✝ a : α
⊢ a ∈ support (uniformOfFinset s hs) ↔ a ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
t : Set α
x : α
⊢ (if x ∈ t then ↑(uniformOfFinset s hs) x else 0) = if x ∈ s ∧ x ∈ t then (↑(Finset.card s))⁻¹ else 0
[PROOFSTEP]
simp_rw [uniformOfFinset_apply, ← ite_and, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
t : Set α
x : α
hx : x ∈ Finset.filter (fun x => x ∈ t) s
⊢ (if x ∈ s ∧ x ∈ t then (↑(Finset.card s))⁻¹ else 0) = (↑(Finset.card s))⁻¹
[PROOFSTEP]
let this : x ∈ s ∧ x ∈ t := by simpa using hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
t : Set α
x : α
hx : x ∈ Finset.filter (fun x => x ∈ t) s
⊢ x ∈ s ∧ x ∈ t
[PROOFSTEP]
simpa using hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
t : Set α
x : α
hx : x ∈ Finset.filter (fun x => x ∈ t) s
this : x ∈ s ∧ x ∈ t := Eq.mp Mathlib.Data.Finset.Basic._auxLemma.130 hx
⊢ (if x ∈ s ∧ x ∈ t then (↑(Finset.card s))⁻¹ else 0) = (↑(Finset.card s))⁻¹
[PROOFSTEP]
simp only [this, and_self_iff, if_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
t : Set α
⊢ ∑ _x in Finset.filter (fun x => x ∈ t) s, (↑(Finset.card s))⁻¹ =
    ↑(Finset.card (Finset.filter (fun x => x ∈ t) s)) / ↑(Finset.card s)
[PROOFSTEP]
simp only [div_eq_mul_inv, Finset.sum_const, nsmul_eq_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Nonempty α
a : α
⊢ ↑(uniformOfFintype α) a = (↑(Fintype.card α))⁻¹
[PROOFSTEP]
simp [uniformOfFintype, Finset.mem_univ, if_true, uniformOfFinset_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Nonempty α
a : α
⊢ Finset.card Finset.univ = Fintype.card α
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α✝
inst✝² : Nonempty α✝
α : Type u_4
inst✝¹ : Fintype α
inst✝ : Nonempty α
x : α
⊢ x ∈ support (uniformOfFintype α) ↔ x ∈ ⊤
[PROOFSTEP]
simp [mem_support_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Nonempty α
a : α
⊢ a ∈ support (uniformOfFintype α)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Nonempty α
s : Set α
⊢ ↑(toOuterMeasure (uniformOfFintype α)) s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)
[PROOFSTEP]
rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_ofFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Nonempty α
s : Set α
⊢ ↑(Finset.card (Finset.filter (fun x => x ∈ s) Finset.univ)) / ↑(Finset.card Finset.univ) =
    ↑(Finset.card (Finset.filter (fun x => x ∈ s) Finset.univ)) / ↑(Fintype.card α)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
inst✝¹ : Nonempty α
s : Set α
inst✝ : MeasurableSpace α
hs : MeasurableSet s
⊢ ↑↑(toMeasure (uniformOfFintype α)) s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)
[PROOFSTEP]
simp [uniformOfFintype, hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
inst✝¹ : Nonempty α
s : Set α
inst✝ : MeasurableSpace α
hs : MeasurableSet s
⊢ ↑(Finset.card (Finset.filter (fun x => x ∈ s) Finset.univ)) / ↑(Finset.card Finset.univ) =
    ↑(Finset.card (Finset.filter (fun x => x ∈ s) Finset.univ)) / ↑(Fintype.card α)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
⊢ ∑' (b : α), ↑(Multiset.count b s) / ↑(↑Multiset.card s) = (↑(↑Multiset.card s))⁻¹ * ∑' (b : α), ↑(Multiset.count b s)
[PROOFSTEP]
simp_rw [ENNReal.div_eq_inv_mul, ENNReal.tsum_mul_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
a : α
ha : ¬a ∈ Multiset.toFinset s
⊢ Multiset.count a s = 0
[PROOFSTEP]
rwa [Multiset.count_eq_zero, ← Multiset.mem_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
⊢ (↑(↑Multiset.card s))⁻¹ * ∑ b in Multiset.toFinset s, ↑(Multiset.count b s) = 1
[PROOFSTEP]
rw [← Nat.cast_sum, Multiset.toFinset_sum_count_eq s,
  ENNReal.inv_mul_cancel (Nat.cast_ne_zero.2 (hs ∘ Multiset.card_eq_zero.1)) (ENNReal.nat_ne_top _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
⊢ ∀ (x : α), x ∈ support (ofMultiset s hs) ↔ x ∈ ↑(Multiset.toFinset s)
[PROOFSTEP]
simp [mem_support_iff, hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
a : α
⊢ a ∈ support (ofMultiset s hs) ↔ a ∈ Multiset.toFinset s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
a : α
ha : ¬a ∈ s
⊢ ↑(ofMultiset s hs) a = 0
[PROOFSTEP]
simpa only [ofMultiset_apply, ENNReal.div_eq_zero_iff, Nat.cast_eq_zero, Multiset.count_eq_zero, ENNReal.nat_ne_top,
  or_false_iff] using ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ ↑(toOuterMeasure (ofMultiset s hs)) t =
    (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s))) / ↑(↑Multiset.card s)
[PROOFSTEP]
simp_rw [div_eq_mul_inv, ← ENNReal.tsum_mul_right, toOuterMeasure_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ ∑' (x : α), Set.indicator t (↑(ofMultiset s hs)) x =
    ∑' (i : α), ↑(Multiset.count i (Multiset.filter (fun x => x ∈ t) s)) * (↑(↑Multiset.card s))⁻¹
[PROOFSTEP]
refine' tsum_congr fun x => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
⊢ Set.indicator t (↑(ofMultiset s hs)) x =
    ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s)) * (↑(↑Multiset.card s))⁻¹
[PROOFSTEP]
by_cases hx : x ∈ t
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
hx : x ∈ t
⊢ Set.indicator t (↑(ofMultiset s hs)) x =
    ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s)) * (↑(↑Multiset.card s))⁻¹
[PROOFSTEP]
simp [Set.indicator, hx, div_eq_mul_inv]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
hx : ¬x ∈ t
⊢ Set.indicator t (↑(ofMultiset s hs)) x =
    ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s)) * (↑(↑Multiset.card s))⁻¹
[PROOFSTEP]
simp [Set.indicator, hx, div_eq_mul_inv]


[GOAL]
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : TopologicalSpace F
hm : m ≤ mΩ
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (id ω, id ω)) μ)
[PROOFSTEP]
rw [← aestronglyMeasurable_comp_snd_map_prod_mk_iff (measurable_id'' hm)] at hf
[GOAL]
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : TopologicalSpace F
hm : m ≤ mΩ
hf : AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (id ω, ω)) μ)
⊢ AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (id ω, id ω)) μ)
[PROOFSTEP]
simp_rw [id.def] at hf ⊢
[GOAL]
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : TopologicalSpace F
hm : m ≤ mΩ
hf : AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (ω, ω)) μ)
⊢ AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (ω, ω)) μ)
[PROOFSTEP]
exact hf
[GOAL]
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : NormedAddCommGroup F
hm : m ≤ mΩ
hf : Integrable f
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
rw [← integrable_comp_snd_map_prod_mk_iff (measurable_id'' hm)] at hf
[GOAL]
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : NormedAddCommGroup F
hm : m ≤ mΩ
hf : Integrable fun x => f x.snd
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
simp_rw [id.def] at hf ⊢
[GOAL]
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : NormedAddCommGroup F
hm : m ≤ mΩ
hf : Integrable fun x => f x.snd
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
exact hf
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁴ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝³ : PolishSpace Ω
inst✝² : BorelSpace Ω
inst✝¹ : Nonempty Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
ω : Ω
⊢ ↑(condexpKernel μ m) ω = ↑(condDistrib id id μ) (id ω)
[PROOFSTEP]
simp_rw [condexpKernel, kernel.comap_apply]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁴ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝³ : PolishSpace Ω
inst✝² : BorelSpace Ω
inst✝¹ : Nonempty Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ IsMarkovKernel (condexpKernel μ m)
[PROOFSTEP]
simp only [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁴ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝³ : PolishSpace Ω
inst✝² : BorelSpace Ω
inst✝¹ : Nonempty Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ IsMarkovKernel (kernel.comap (condDistrib id id μ) id (_ : Measurable id))
[PROOFSTEP]
infer_instance
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
s : Set Ω
hs : MeasurableSet s
⊢ Measurable fun ω => ↑↑(↑(condexpKernel μ m) ω) s
[PROOFSTEP]
simp_rw [condexpKernel_apply_eq_condDistrib]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
s : Set Ω
hs : MeasurableSet s
⊢ Measurable fun ω => ↑↑(↑(condDistrib id id μ) (id ω)) s
[PROOFSTEP]
refine Measurable.mono ?_ (inf_le_left : m ⊓ mΩ ≤ m) le_rfl
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
s : Set Ω
hs : MeasurableSet s
⊢ Measurable fun ω => ↑↑(↑(condDistrib id id μ) (id ω)) s
[PROOFSTEP]
convert measurable_condDistrib (μ := μ) hs
[GOAL]
case h.e'_3
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
s : Set Ω
hs : MeasurableSet s
⊢ m ⊓ mΩ = MeasurableSpace.comap id (m ⊓ mΩ)
[PROOFSTEP]
rw [MeasurableSpace.comap_id]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂↑(condexpKernel μ m) ω) μ
[PROOFSTEP]
simp_rw [condexpKernel_apply_eq_condDistrib]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂↑(condDistrib id id μ) (id ω)) μ
[PROOFSTEP]
exact
  AEStronglyMeasurable.integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf.comp_snd_map_prod_id inf_le_right)
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y ∂↑(condexpKernel μ m) ω) μ
[PROOFSTEP]
rw [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y ∂↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω) μ
[PROOFSTEP]
have h :=
  aestronglyMeasurable'_integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : AEStronglyMeasurable f μ
h :
  AEStronglyMeasurable' (MeasurableSpace.comap id (m ⊓ mΩ))
    (fun a => ∫ (y : Ω), f (id a, y).snd ∂↑(condDistrib id id μ) (id a)) μ
⊢ AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y ∂↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω) μ
[PROOFSTEP]
rw [MeasurableSpace.comap_id] at h
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : AEStronglyMeasurable f μ
h : AEStronglyMeasurable' (m ⊓ mΩ) (fun a => ∫ (y : Ω), f (id a, y).snd ∂↑(condDistrib id id μ) (id a)) μ
⊢ AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y ∂↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω) μ
[PROOFSTEP]
exact AEStronglyMeasurable'.mono h inf_le_left
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f
[PROOFSTEP]
rw [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f
[PROOFSTEP]
exact
  Integrable.condDistrib_ae (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f
⊢ Integrable fun ω => ∫ (y : Ω), ‖f y‖ ∂↑(condexpKernel μ m) ω
[PROOFSTEP]
rw [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f
⊢ Integrable fun ω => ∫ (y : Ω), ‖f y‖ ∂↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω
[PROOFSTEP]
exact
  Integrable.integral_norm_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
⊢ Integrable fun ω => ‖∫ (y : Ω), f y ∂↑(condexpKernel μ m) ω‖
[PROOFSTEP]
rw [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
⊢ Integrable fun ω => ‖∫ (y : Ω), f y ∂↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω‖
[PROOFSTEP]
exact
  Integrable.norm_integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
⊢ Integrable fun ω => ∫ (y : Ω), f y ∂↑(condexpKernel μ m) ω
[PROOFSTEP]
rw [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
⊢ Integrable fun ω => ∫ (y : Ω), f y ∂↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω
[PROOFSTEP]
exact
  Integrable.integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
s : Set Ω
hs : MeasurableSet s
⊢ Integrable fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)
[PROOFSTEP]
rw [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
s : Set Ω
hs : MeasurableSet s
⊢ Integrable fun ω => ENNReal.toReal (↑↑(↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω) s)
[PROOFSTEP]
exact integrable_toReal_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) hs
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
⊢ (fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m ⊓ mΩ]
[PROOFSTEP]
have h := condDistrib_ae_eq_condexp (μ := μ) (measurable_id'' (inf_le_right : m ⊓ mΩ ≤ mΩ)) measurable_id hs
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h :
  (fun a => ENNReal.toReal (↑↑(↑(condDistrib id id μ) (id a)) s)) =ᵐ[μ]
    μ[indicator (id ⁻¹' s) fun ω => 1|MeasurableSpace.comap id (m ⊓ mΩ)]
⊢ (fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m ⊓ mΩ]
[PROOFSTEP]
simp only [id_eq, ge_iff_le, MeasurableSpace.comap_id, preimage_id_eq] at h
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : (fun a => ENNReal.toReal (↑↑(↑(condDistrib id id μ) a) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m ⊓ mΩ]
⊢ (fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m ⊓ mΩ]
[PROOFSTEP]
simp_rw [condexpKernel_apply_eq_condDistrib]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : (fun a => ENNReal.toReal (↑↑(↑(condDistrib id id μ) a) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m ⊓ mΩ]
⊢ (fun ω => ENNReal.toReal (↑↑(↑(condDistrib id id μ) (id ω)) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m ⊓ mΩ]
[PROOFSTEP]
exact h
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ μ[indicator s fun ω => 1|m ⊓ mΩ] =ᵐ[μ] μ[indicator s fun ω => 1|m]
[PROOFSTEP]
rw [inf_of_le_left hm]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)) =ᵐ[Measure.trim μ hm] μ[indicator s fun ω => 1|m]
[PROOFSTEP]
rw [ae_eq_trim_iff hm _ stronglyMeasurable_condexp]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m]
[PROOFSTEP]
exact condexpKernel_ae_eq_condexp hm hs
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ StronglyMeasurable fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)
[PROOFSTEP]
refine Measurable.stronglyMeasurable ?_
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ Measurable fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)
[PROOFSTEP]
exact @Measurable.ennreal_toReal _ m _ (measurable_condexpKernel hs)
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
⊢ μ[f|m ⊓ mΩ] =ᵐ[μ] fun ω => ∫ (y : Ω), f y ∂↑(condexpKernel μ m) ω
[PROOFSTEP]
have hX : @Measurable Ω Ω mΩ (m ⊓ mΩ) id := measurable_id.mono le_rfl (inf_le_right : m ⊓ mΩ ≤ mΩ)
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
hX : Measurable id
⊢ μ[f|m ⊓ mΩ] =ᵐ[μ] fun ω => ∫ (y : Ω), f y ∂↑(condexpKernel μ m) ω
[PROOFSTEP]
simp_rw [condexpKernel_apply_eq_condDistrib]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
hX : Measurable id
⊢ μ[f|m ⊓ mΩ] =ᵐ[μ] fun ω => ∫ (y : Ω), f y ∂↑(condDistrib id id μ) (id ω)
[PROOFSTEP]
have h := condexp_ae_eq_integral_condDistrib_id hX hf_int
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
hX : Measurable id
h : μ[f|MeasurableSpace.comap id (m ⊓ mΩ)] =ᵐ[μ] fun a => ∫ (y : Ω), f y ∂↑(condDistrib id id μ) (id a)
⊢ μ[f|m ⊓ mΩ] =ᵐ[μ] fun ω => ∫ (y : Ω), f y ∂↑(condDistrib id id μ) (id ω)
[PROOFSTEP]
simpa only [MeasurableSpace.comap_id, id_eq] using h
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f
⊢ μ[f|m ⊓ mΩ] =ᵐ[μ] μ[f|m]
[PROOFSTEP]
rw [inf_of_le_left hm]