[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → { x // x ∈ kernel α β }
a : α
⊢ ↑(∑ i in I, κ i) a = ∑ i in I, ↑(κ i) a
[PROOFSTEP]
rw [coe_finset_sum, Finset.sum_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → { x // x ∈ kernel α β }
a : α
s : Set β
⊢ ↑↑(↑(∑ i in I, κ i) a) s = ∑ i in I, ↑↑(↑(κ i) a) s
[PROOFSTEP]
rw [finset_sum_apply, Measure.finset_sum_apply]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
mα✝ : MeasurableSpace α✝
mβ✝ : MeasurableSpace β✝
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
x✝ : α
⊢ ↑↑(↑0 x✝) Set.univ ≤ 0
[PROOFSTEP]
simp only [kernel.zero_apply, Measure.coe_zero, Pi.zero_apply, le_zero_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel (κ + η)
[PROOFSTEP]
refine
  ⟨⟨IsFiniteKernel.bound κ + IsFiniteKernel.bound η,
      ENNReal.add_lt_top.mpr ⟨IsFiniteKernel.bound_lt_top κ, IsFiniteKernel.bound_lt_top η⟩, fun a => ?_⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ↑↑(↑(κ + η) a) Set.univ ≤ bound κ + bound η
[PROOFSTEP]
exact add_le_add (kernel.measure_le_bound _ _ _) (kernel.measure_le_bound _ _ _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
⊢ κ = η ↔ ∀ (a : α) (s : Set β), MeasurableSet s → ↑↑(↑κ a) s = ↑↑(↑η a) s
[PROOFSTEP]
simp_rw [ext_iff, Measure.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
h : ∀ (a : α) (f : β → ℝ≥0∞), Measurable f → ∫⁻ (b : β), f b ∂↑κ a = ∫⁻ (b : β), f b ∂↑η a
⊢ κ = η
[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 α β }
h : ∀ (a : α) (f : β → ℝ≥0∞), Measurable f → ∫⁻ (b : β), f b ∂↑κ a = ∫⁻ (b : β), f b ∂↑η a
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑κ a) s = ↑↑(↑η a) s
[PROOFSTEP]
specialize h a (s.indicator fun _ => 1) (Measurable.indicator measurable_const hs)
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
a : α
s : Set β
hs : MeasurableSet s
h : ∫⁻ (b : β), Set.indicator s (fun x => 1) b ∂↑κ a = ∫⁻ (b : β), Set.indicator s (fun x => 1) b ∂↑η a
⊢ ↑↑(↑κ a) s = ↑↑(↑η a) s
[PROOFSTEP]
simp_rw [lintegral_indicator_const hs, one_mul] at h 
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
a : α
s : Set β
hs : MeasurableSet s
h : ↑↑(↑κ a) s = ↑↑(↑η a) s
⊢ ↑↑(↑κ a) s = ↑↑(↑η a) s
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
h : κ = η
a : α
f : β → ℝ≥0∞
x✝ : Measurable f
⊢ ∫⁻ (b : β), f b ∂↑κ a = ∫⁻ (b : β), f b ∂↑η a
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ Integrable fun x => ENNReal.toReal (↑↑(↑κ x) s)
[PROOFSTEP]
refine'
  Integrable.mono' (integrable_const (IsFiniteKernel.bound κ).toReal)
    ((kernel.measurable_coe κ hs).ennreal_toReal.aestronglyMeasurable) (ae_of_all μ <| fun x => _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
x : α
⊢ ‖ENNReal.toReal (↑↑(↑κ x) s)‖ ≤ ENNReal.toReal (IsFiniteKernel.bound κ)
[PROOFSTEP]
rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg,
  ENNReal.toReal_le_toReal (measure_ne_top _ _) (IsFiniteKernel.bound_ne_top _)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
x : α
⊢ ↑↑(↑κ x) s ≤ IsFiniteKernel.bound κ
[PROOFSTEP]
exact kernel.measure_le_bound _ _ _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κ : ι → { x // x ∈ kernel α β }
⊢ (fun a => Measure.sum fun n => ↑(κ n) 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 α β }
inst✝ : Countable ι
κ : ι → { x // x ∈ kernel α β }
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(Measure.sum fun n => ↑(κ n) b) s
[PROOFSTEP]
simp_rw [Measure.sum_apply _ hs]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κ : ι → { x // x ∈ kernel α β }
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ∑' (i : ι), ↑↑(↑(κ i) b) s
[PROOFSTEP]
exact Measurable.ennreal_tsum fun n => kernel.measurable_coe (κ n) hs
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κ : ι → { x // x ∈ kernel α β }
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(kernel.sum κ) a) s = ∑' (n : ι), ↑↑(↑(κ n) a) s
[PROOFSTEP]
rw [sum_apply κ a, Measure.sum_apply _ hs]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
⊢ (kernel.sum fun x => 0) = 0
[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 α β }
inst✝ : Countable ι
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(kernel.sum fun x => 0) a) s = ↑↑(↑0 a) s
[PROOFSTEP]
rw [sum_apply' _ a hs]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (n : ι), ↑↑(↑0 a) s = ↑↑(↑0 a) s
[PROOFSTEP]
simp only [zero_apply, Measure.coe_zero, Pi.zero_apply, tsum_zero]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κ : ι → ι → { x // x ∈ kernel α β }
⊢ (kernel.sum fun n => kernel.sum (κ n)) = kernel.sum fun m => kernel.sum fun n => κ n m
[PROOFSTEP]
ext a s
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κ : ι → ι → { x // x ∈ kernel α β }
a : α
s : Set β
a✝ : MeasurableSet s
⊢ ↑↑(↑(kernel.sum fun n => kernel.sum (κ n)) a) s = ↑↑(↑(kernel.sum fun m => kernel.sum fun n => κ n m) a) s
[PROOFSTEP]
simp_rw [sum_apply]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κ : ι → ι → { x // x ∈ kernel α β }
a : α
s : Set β
a✝ : MeasurableSet s
⊢ ↑↑(Measure.sum fun n => Measure.sum fun n_1 => ↑(κ n n_1) a) s =
    ↑↑(Measure.sum fun n => Measure.sum fun n_1 => ↑(κ n_1 n) a) s
[PROOFSTEP]
rw [Measure.sum_comm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
inst✝ : Fintype ι
κ : ι → { x // x ∈ kernel α β }
⊢ kernel.sum κ = ∑ i : ι, κ i
[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 α β }
inst✝ : Fintype ι
κ : ι → { x // x ∈ kernel α β }
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(kernel.sum κ) a) s = ↑↑(↑(∑ i : ι, κ i) a) s
[PROOFSTEP]
simp only [sum_apply' κ a hs, finset_sum_apply' _ κ a s, tsum_fintype]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κ η : ι → { x // x ∈ kernel α β }
⊢ (kernel.sum fun n => κ n + η n) = kernel.sum κ + kernel.sum η
[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 α β }
inst✝ : Countable ι
κ η : ι → { x // x ∈ kernel α β }
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(kernel.sum fun n => κ n + η n) a) s = ↑↑(↑(kernel.sum κ + kernel.sum η) a) s
[PROOFSTEP]
simp only [coeFn_add, Pi.add_apply, sum_apply, Measure.sum_apply _ hs, Pi.add_apply, Measure.coe_add,
  tsum_add ENNReal.summable ENNReal.summable]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
h : IsFiniteKernel κ
n : ℕ
⊢ IsFiniteKernel ((fun n => if n = 0 then κ else 0) n)
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
h : IsFiniteKernel κ
n : ℕ
⊢ IsFiniteKernel (if n = 0 then κ else 0)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
h : IsFiniteKernel κ
n : ℕ
h✝ : n = 0
⊢ IsFiniteKernel κ
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
h : IsFiniteKernel κ
n : ℕ
h✝ : ¬n = 0
⊢ IsFiniteKernel 0
[PROOFSTEP]
exact h
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
h : IsFiniteKernel κ
n : ℕ
h✝ : ¬n = 0
⊢ IsFiniteKernel 0
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
h : IsFiniteKernel κ
⊢ κ = kernel.sum fun n => if n = 0 then κ else 0
[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 α β }
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑κ a) s = ↑↑(↑(kernel.sum fun n => if n = 0 then κ else 0) a) s
[PROOFSTEP]
rw [kernel.sum_apply' _ _ hs]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑κ a) s = ∑' (n : ℕ), ↑↑(↑(if n = 0 then κ else 0) a) s
[PROOFSTEP]
have : (fun i => ((ite (i = 0) κ 0) a) s) = fun i => ite (i = 0) (κ a s) 0 := by ext1 i; split_ifs <;> rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
⊢ (fun i => ↑↑(↑(if i = 0 then κ else 0) a) s) = fun i => if i = 0 then ↑↑(↑κ a) s else 0
[PROOFSTEP]
ext1 i
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
⊢ ↑↑(↑(if i = 0 then κ else 0) a) s = if i = 0 then ↑↑(↑κ a) s else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
h✝ : i = 0
⊢ ↑↑(↑κ a) s = ↑↑(↑κ a) s
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
h✝ : ¬i = 0
⊢ ↑↑(↑0 a) s = 0
[PROOFSTEP]
rfl
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
this : (fun i => ↑↑(↑(if i = 0 then κ else 0) a) s) = fun i => if i = 0 then ↑↑(↑κ a) s else 0
⊢ ↑↑(↑κ a) s = ∑' (n : ℕ), ↑↑(↑(if n = 0 then κ else 0) a) s
[PROOFSTEP]
rw [this, tsum_ite_eq]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ κ : { x // x ∈ kernel α β }
h : IsSFiniteKernel κ
a : α
⊢ (Measure.sum fun n => ↑(seq κ n) a) = ↑κ a
[PROOFSTEP]
rw [← kernel.sum_apply, kernel_sum_seq κ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ κ η : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ IsSFiniteKernel (κ + η)
[PROOFSTEP]
refine' ⟨⟨fun n => seq κ n + seq η n, fun n => inferInstance, _⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ κ η : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ κ + η = kernel.sum fun n => seq κ n + seq η n
[PROOFSTEP]
rw [sum_add, kernel_sum_seq κ, kernel_sum_seq η]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I : Finset ι
h : ∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel (∑ i in I, κs i)
[PROOFSTEP]
classical
induction' I using Finset.induction with i I hi_nmem_I h_ind h
· rw [Finset.sum_empty]; infer_instance
· rw [Finset.sum_insert hi_nmem_I]
  haveI : IsSFiniteKernel (κs i) := h i (Finset.mem_insert_self _ _)
  have : IsSFiniteKernel (∑ x : ι in I, κs x) := h_ind fun i hiI => h i (Finset.mem_insert_of_mem hiI)
  exact IsSFiniteKernel.add _ _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I : Finset ι
h : ∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel (∑ i in I, κs i)
[PROOFSTEP]
induction' I using Finset.induction with i I hi_nmem_I h_ind h
[GOAL]
case empty
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I : Finset ι
h✝ : ∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)
h : ∀ (i : ι), i ∈ ∅ → IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel (∑ i in ∅, κs i)
[PROOFSTEP]
rw [Finset.sum_empty]
[GOAL]
case empty
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I : Finset ι
h✝ : ∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)
h : ∀ (i : ι), i ∈ ∅ → IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel 0
[PROOFSTEP]
infer_instance
[GOAL]
case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ I✝ → IsSFiniteKernel (κs i)
i : ι
I : Finset ι
hi_nmem_I : ¬i ∈ I
h_ind : (∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i in I, κs i)
h : ∀ (i_1 : ι), i_1 ∈ insert i I → IsSFiniteKernel (κs i_1)
⊢ IsSFiniteKernel (∑ i in insert i I, κs i)
[PROOFSTEP]
rw [Finset.sum_insert hi_nmem_I]
[GOAL]
case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ I✝ → IsSFiniteKernel (κs i)
i : ι
I : Finset ι
hi_nmem_I : ¬i ∈ I
h_ind : (∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i in I, κs i)
h : ∀ (i_1 : ι), i_1 ∈ insert i I → IsSFiniteKernel (κs i_1)
⊢ IsSFiniteKernel (κs i + ∑ x in I, κs x)
[PROOFSTEP]
haveI : IsSFiniteKernel (κs i) := h i (Finset.mem_insert_self _ _)
[GOAL]
case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ I✝ → IsSFiniteKernel (κs i)
i : ι
I : Finset ι
hi_nmem_I : ¬i ∈ I
h_ind : (∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i in I, κs i)
h : ∀ (i_1 : ι), i_1 ∈ insert i I → IsSFiniteKernel (κs i_1)
this : IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel (κs i + ∑ x in I, κs x)
[PROOFSTEP]
have : IsSFiniteKernel (∑ x : ι in I, κs x) := h_ind fun i hiI => h i (Finset.mem_insert_of_mem hiI)
[GOAL]
case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ I✝ → IsSFiniteKernel (κs i)
i : ι
I : Finset ι
hi_nmem_I : ¬i ∈ I
h_ind : (∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i in I, κs i)
h : ∀ (i_1 : ι), i_1 ∈ insert i I → IsSFiniteKernel (κs i_1)
this✝ : IsSFiniteKernel (κs i)
this : IsSFiniteKernel (∑ x in I, κs x)
⊢ IsSFiniteKernel (κs i + ∑ x in I, κs x)
[PROOFSTEP]
exact IsSFiniteKernel.add _ _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
⊢ IsSFiniteKernel (kernel.sum κs)
[PROOFSTEP]
let e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ IsSFiniteKernel (kernel.sum κs)
[PROOFSTEP]
refine' ⟨⟨fun n => seq (κs (e n).1) (e n).2, inferInstance, _⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ kernel.sum κs = kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd
[PROOFSTEP]
have hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n)) := by simp_rw [kernel_sum_seq]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
[PROOFSTEP]
simp_rw [kernel_sum_seq]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
⊢ kernel.sum κs = kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd
[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 α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(kernel.sum κs) a) s = ↑↑(↑(kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd) a) s
[PROOFSTEP]
rw [hκ_eq]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(kernel.sum fun n => kernel.sum (seq (κs n))) a) s = ↑↑(↑(kernel.sum fun n => seq (κs (↑e n).fst) (↑e n).snd) a) s
[PROOFSTEP]
simp_rw [kernel.sum_apply' _ _ hs]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (n : ι) (n_1 : ℕ), ↑↑(↑(seq (κs n) n_1) a) s =
    ∑' (n : ℕ), ↑↑(↑(seq (κs (↑(Denumerable.eqv (ι × ℕ)).symm n).fst) (↑(Denumerable.eqv (ι × ℕ)).symm n).snd) a) s
[PROOFSTEP]
change (∑' i, ∑' m, seq (κs i) m a s) = ∑' n, (fun im : ι × ℕ => seq (κs im.fst) im.snd a s) (e n)
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Denumerable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : kernel.sum κs = kernel.sum fun n => kernel.sum (seq (κs n))
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ι) (m : ℕ), ↑↑(↑(seq (κs i) m) a) s = ∑' (n : ℕ), (fun im => ↑↑(↑(seq (κs im.fst) im.snd) a) s) (↑e n)
[PROOFSTEP]
rw [e.tsum_eq (fun im : ι × ℕ => seq (κs im.fst) im.snd a s), tsum_prod' ENNReal.summable fun _ => ENNReal.summable]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
⊢ IsSFiniteKernel (kernel.sum κs)
[PROOFSTEP]
cases fintypeOrInfinite ι
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝ : Fintype ι
⊢ IsSFiniteKernel (kernel.sum κs)
[PROOFSTEP]
rw [sum_fintype]
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝ : Fintype ι
⊢ IsSFiniteKernel (∑ i : ι, κs i)
[PROOFSTEP]
exact IsSFiniteKernel.finset_sum Finset.univ fun i _ => hκs i
[GOAL]
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝ : Infinite ι
⊢ IsSFiniteKernel (kernel.sum κs)
[PROOFSTEP]
cases nonempty_denumerable ι
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝¹ : Infinite ι
val✝ : Denumerable ι
⊢ IsSFiniteKernel (kernel.sum κs)
[PROOFSTEP]
exact isSFiniteKernel_sum_of_denumerable hκs
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : α → β
hf : Measurable f
⊢ (fun a => Measure.dirac (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 : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(Measure.dirac (f b)) s
[PROOFSTEP]
simp_rw [Measure.dirac_apply' _ hs]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => Set.indicator s 1 (f b)
[PROOFSTEP]
exact measurable_one.indicator (hf hs)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(deterministic f hf) a) s = Set.indicator s (fun x => 1) (f a)
[PROOFSTEP]
rw [deterministic]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑{ val := fun a => Measure.dirac (f a), property := (_ : Measurable fun a => Measure.dirac (f a)) } a) s =
    Set.indicator s (fun x => 1) (f a)
[PROOFSTEP]
change Measure.dirac (f a) s = s.indicator 1 (f a)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(Measure.dirac (f a)) s = Set.indicator s 1 (f a)
[PROOFSTEP]
simp_rw [Measure.dirac_apply' _ hs]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : α → β
hf : Measurable f
a : α
⊢ IsProbabilityMeasure (↑(deterministic f hf) a)
[PROOFSTEP]
rw [deterministic_apply hf]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : α → β
hf : Measurable f
a : α
⊢ IsProbabilityMeasure (Measure.dirac (f a))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
⊢ ∫⁻ (x : β), f x ∂↑(deterministic g hg) a = f (g a)
[PROOFSTEP]
rw [kernel.deterministic_apply, lintegral_dirac' _ hf]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst✝ : MeasurableSingletonClass β
⊢ ∫⁻ (x : β), f x ∂↑(deterministic g hg) a = f (g a)
[PROOFSTEP]
rw [kernel.deterministic_apply, lintegral_dirac (g a) f]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
s : Set β
hs : MeasurableSet s
inst✝ : Decidable (g a ∈ s)
⊢ ∫⁻ (x : β) in s, f x ∂↑(deterministic g hg) a = if g a ∈ s then f (g a) else 0
[PROOFSTEP]
rw [kernel.deterministic_apply, set_lintegral_dirac' hf hs]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst✝¹ : MeasurableSingletonClass β
s : Set β
inst✝ : Decidable (g a ∈ s)
⊢ ∫⁻ (x : β) in s, f x ∂↑(deterministic g hg) a = if g a ∈ s then f (g a) else 0
[PROOFSTEP]
rw [kernel.deterministic_apply, set_lintegral_dirac f s]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : β → E
g : α → β
a : α
hg : Measurable g
hf : StronglyMeasurable f
⊢ ∫ (x : β), f x ∂↑(deterministic g hg) a = f (g a)
[PROOFSTEP]
rw [kernel.deterministic_apply, integral_dirac' _ _ hf]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : β → E
g : α → β
a : α
hg : Measurable g
inst✝ : MeasurableSingletonClass β
⊢ ∫ (x : β), f x ∂↑(deterministic g hg) a = f (g a)
[PROOFSTEP]
rw [kernel.deterministic_apply, integral_dirac _ (g a)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : β → E
g : α → β
a : α
hg : Measurable g
hf : StronglyMeasurable f
s : Set β
hs : MeasurableSet s
inst✝ : Decidable (g a ∈ s)
⊢ ∫ (x : β) in s, f x ∂↑(deterministic g hg) a = if g a ∈ s then f (g a) else 0
[PROOFSTEP]
rw [kernel.deterministic_apply, set_integral_dirac' hf _ hs]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : β → E
g : α → β
a : α
hg : Measurable g
inst✝¹ : MeasurableSingletonClass β
s : Set β
inst✝ : Decidable (g a ∈ s)
⊢ ∫ (x : β) in s, f x ∂↑(deterministic g hg) a = if g a ∈ s then f (g a) else 0
[PROOFSTEP]
rw [kernel.deterministic_apply, set_integral_dirac f _ s]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : β → ℝ≥0∞
μ : Measure β
a : α
⊢ ∫⁻ (x : β), f x ∂↑(const α μ) a = ∫⁻ (x : β), f x ∂μ
[PROOFSTEP]
rw [kernel.const_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : β → ℝ≥0∞
μ : Measure β
a : α
s : Set β
⊢ ∫⁻ (x : β) in s, f x ∂↑(const α μ) a = ∫⁻ (x : β) in s, f x ∂μ
[PROOFSTEP]
rw [kernel.const_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
μ : Measure β
a : α
⊢ ∫ (x : β), f x ∂↑(const α μ) a = ∫ (x : β), f x ∂μ
[PROOFSTEP]
rw [kernel.const_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
μ : Measure β
a : α
s : Set β
⊢ ∫ (x : β) in s, f x ∂↑(const α μ) a = ∫ (x : β) in s, f x ∂μ
[PROOFSTEP]
rw [kernel.const_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t : Set β
κ : { x // x ∈ kernel α β }
hs : MeasurableSet s
⊢ (fun a => Measure.restrict (↑κ a) s) ∈ kernel α β
[PROOFSTEP]
refine' Measure.measurable_of_measurable_coe _ fun t ht => _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t✝ : Set β
κ : { x // x ∈ kernel α β }
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ Measurable fun b => ↑↑(Measure.restrict (↑κ b) s) t
[PROOFSTEP]
simp_rw [Measure.restrict_apply ht]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t✝ : Set β
κ : { x // x ∈ kernel α β }
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ Measurable fun b => ↑↑(↑κ b) (t ∩ s)
[PROOFSTEP]
exact kernel.measurable_coe κ (ht.inter hs)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t : Set β
κ : { x // x ∈ kernel α β }
hs : MeasurableSet s
a : α
ht : MeasurableSet t
⊢ ↑↑(↑(kernel.restrict κ hs) a) t = ↑↑(↑κ a) (t ∩ s)
[PROOFSTEP]
rw [restrict_apply κ hs a, Measure.restrict_apply ht]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
s t : Set β
⊢ kernel.restrict κ (_ : MeasurableSet Set.univ) = κ
[PROOFSTEP]
ext1 a
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
s t : Set β
a : α
⊢ ↑(kernel.restrict κ (_ : MeasurableSet Set.univ)) a = ↑κ a
[PROOFSTEP]
rw [kernel.restrict_apply, Measure.restrict_univ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t : Set β
κ : { x // x ∈ kernel α β }
hs : MeasurableSet s
a : α
f : β → ℝ≥0∞
⊢ ∫⁻ (b : β), f b ∂↑(kernel.restrict κ hs) a = ∫⁻ (b : β) in s, f b ∂↑κ a
[PROOFSTEP]
rw [restrict_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t✝ : Set β
κ : { x // x ∈ kernel α β }
hs : MeasurableSet s
a : α
f : β → ℝ≥0∞
t : Set β
⊢ ∫⁻ (b : β) in t, f b ∂↑(kernel.restrict κ hs) a = ∫⁻ (b : β) in t ∩ s, f b ∂↑κ a
[PROOFSTEP]
rw [restrict_apply, Measure.restrict_restrict' hs]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
s t✝ : Set β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
hs : MeasurableSet s
t : Set β
⊢ ∫ (x : β) in t, f x ∂↑(kernel.restrict κ hs) a = ∫ (x : β) in t ∩ s, f x ∂↑κ a
[PROOFSTEP]
rw [restrict_apply, Measure.restrict_restrict' hs]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t : Set β
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
hs : MeasurableSet s
⊢ IsFiniteKernel (kernel.restrict κ hs)
[PROOFSTEP]
refine' ⟨⟨IsFiniteKernel.bound κ, IsFiniteKernel.bound_lt_top κ, fun a => _⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t : Set β
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
hs : MeasurableSet s
a : α
⊢ ↑↑(↑(kernel.restrict κ hs) a) Set.univ ≤ IsFiniteKernel.bound κ
[PROOFSTEP]
rw [restrict_apply' κ hs a MeasurableSet.univ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t : Set β
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
hs : MeasurableSet s
a : α
⊢ ↑↑(↑κ a) (Set.univ ∩ s) ≤ IsFiniteKernel.bound κ
[PROOFSTEP]
exact measure_le_bound κ a _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t : Set β
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hs : MeasurableSet s
⊢ IsSFiniteKernel (kernel.restrict κ hs)
[PROOFSTEP]
refine' ⟨⟨fun n => kernel.restrict (seq κ n) hs, inferInstance, _⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t : Set β
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hs : MeasurableSet s
⊢ kernel.restrict κ hs = kernel.sum fun n => kernel.restrict (seq κ n) hs
[PROOFSTEP]
ext1 a
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t : Set β
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hs : MeasurableSet s
a : α
⊢ ↑(kernel.restrict κ hs) a = ↑(kernel.sum fun n => kernel.restrict (seq κ n) hs) a
[PROOFSTEP]
simp_rw [sum_apply, restrict_apply, ← Measure.restrict_sum _ hs, ← sum_apply, kernel_sum_seq]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
⊢ (fun a => Measure.comap f (↑κ a)) ∈ kernel α γ
[PROOFSTEP]
refine' Measure.measurable_measure.mpr fun t ht => _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
⊢ Measurable fun b => ↑↑(Measure.comap f (↑κ b)) t
[PROOFSTEP]
have : (fun a => Measure.comap f (κ a) t) = fun a => κ a (f '' t) :=
  by
  ext1 a
  rw [Measure.comap_apply _ hf.injective _ _ ht]
  exact fun s' hs' ↦ hf.measurableSet_image.mpr hs'
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
⊢ (fun a => ↑↑(Measure.comap f (↑κ a)) t) = fun a => ↑↑(↑κ a) (f '' t)
[PROOFSTEP]
ext1 a
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
a : α
⊢ ↑↑(Measure.comap f (↑κ a)) t = ↑↑(↑κ a) (f '' t)
[PROOFSTEP]
rw [Measure.comap_apply _ hf.injective _ _ ht]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
a : α
⊢ ∀ (s : Set γ), MeasurableSet s → MeasurableSet (f '' s)
[PROOFSTEP]
exact fun s' hs' ↦ hf.measurableSet_image.mpr hs'
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
this : (fun a => ↑↑(Measure.comap f (↑κ a)) t) = fun a => ↑↑(↑κ a) (f '' t)
⊢ Measurable fun b => ↑↑(Measure.comap f (↑κ b)) t
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
this : (fun a => ↑↑(Measure.comap f (↑κ a)) t) = fun a => ↑↑(↑κ a) (f '' t)
⊢ Measurable fun a => ↑↑(↑κ a) (f '' t)
[PROOFSTEP]
exact kernel.measurable_coe _ (hf.measurableSet_image.mpr ht)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ ↑↑(↑(comapRight κ hf) a) t = ↑↑(↑κ a) (f '' t)
[PROOFSTEP]
rw [comapRight_apply, Measure.comap_apply _ hf.injective (fun s => hf.measurableSet_image.mpr) _ ht]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
hκ : ∀ (a : α), ↑↑(↑κ a) (Set.range f) = 1
⊢ IsMarkovKernel (kernel.comapRight κ hf)
[PROOFSTEP]
refine' ⟨fun a => ⟨_⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
hκ : ∀ (a : α), ↑↑(↑κ a) (Set.range f) = 1
a : α
⊢ ↑↑(↑(kernel.comapRight κ hf) a) Set.univ = 1
[PROOFSTEP]
rw [comapRight_apply' κ hf a MeasurableSet.univ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
hκ : ∀ (a : α), ↑↑(↑κ a) (Set.range f) = 1
a : α
⊢ ↑↑(↑κ a) (f '' Set.univ) = 1
[PROOFSTEP]
simp only [Set.image_univ, Subtype.range_coe_subtype, Set.setOf_mem_eq]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
hκ : ∀ (a : α), ↑↑(↑κ a) (Set.range f) = 1
a : α
⊢ ↑↑(↑κ a) (Set.range f) = 1
[PROOFSTEP]
exact hκ a
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
hf : MeasurableEmbedding f
⊢ IsFiniteKernel (kernel.comapRight κ hf)
[PROOFSTEP]
refine' ⟨⟨IsFiniteKernel.bound κ, IsFiniteKernel.bound_lt_top κ, fun a => _⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ ↑↑(↑(kernel.comapRight κ hf) a) Set.univ ≤ IsFiniteKernel.bound κ
[PROOFSTEP]
rw [comapRight_apply' κ hf a .univ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
inst✝ : IsFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ ↑↑(↑κ a) (f '' Set.univ) ≤ IsFiniteKernel.bound κ
[PROOFSTEP]
exact measure_le_bound κ a _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
⊢ IsSFiniteKernel (comapRight κ hf)
[PROOFSTEP]
refine' ⟨⟨fun n => comapRight (seq κ n) hf, inferInstance, _⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
⊢ comapRight κ hf = kernel.sum fun n => comapRight (seq κ n) hf
[PROOFSTEP]
ext1 a
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ ↑(comapRight κ hf) a = ↑(kernel.sum fun n => comapRight (seq κ n) hf) a
[PROOFSTEP]
rw [sum_apply]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ ↑(comapRight κ hf) a = Measure.sum fun n => ↑(comapRight (seq κ n) hf) a
[PROOFSTEP]
simp_rw [comapRight_apply _ hf]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ Measure.comap f (↑κ a) = Measure.sum fun n => Measure.comap f (↑(seq κ n) a)
[PROOFSTEP]
have : (Measure.sum fun n => Measure.comap f (seq κ n a)) = Measure.comap f (Measure.sum fun n => seq κ n a) :=
  by
  ext1 t ht
  rw [Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht, Measure.sum_apply _ ht,
    Measure.sum_apply _ (hf.measurableSet_image.mpr ht)]
  congr with n : 1
  rw [Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ (Measure.sum fun n => Measure.comap f (↑(seq κ n) a)) = Measure.comap f (Measure.sum fun n => ↑(seq κ n) a)
[PROOFSTEP]
ext1 t ht
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ ↑↑(Measure.sum fun n => Measure.comap f (↑(seq κ n) a)) t = ↑↑(Measure.comap f (Measure.sum fun n => ↑(seq κ n) a)) t
[PROOFSTEP]
rw [Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht, Measure.sum_apply _ ht,
  Measure.sum_apply _ (hf.measurableSet_image.mpr ht)]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ ∑' (i : ℕ), ↑↑(Measure.comap f (↑(seq κ i) a)) t = ∑' (i : ℕ), ↑↑(↑(seq κ i) a) (f '' t)
[PROOFSTEP]
congr with n : 1
[GOAL]
case h.e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
n : ℕ
⊢ ↑↑(Measure.comap f (↑(seq κ n) a)) t = ↑↑(↑(seq κ n) a) (f '' t)
[PROOFSTEP]
rw [Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
this : (Measure.sum fun n => Measure.comap f (↑(seq κ n) a)) = Measure.comap f (Measure.sum fun n => ↑(seq κ n) a)
⊢ Measure.comap f (↑κ a) = Measure.sum fun n => Measure.comap f (↑(seq κ n) a)
[PROOFSTEP]
rw [this, measure_sum_seq]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
t : Set β
⊢ ↑↑(↑(piecewise hs κ η) a) t = if a ∈ s then ↑↑(↑κ a) t else ↑↑(↑η a) t
[PROOFSTEP]
rw [piecewise_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
t : Set β
⊢ ↑↑(if a ∈ s then ↑κ a else ↑η a) t = if a ∈ s then ↑↑(↑κ a) t else ↑↑(↑η a) t
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
t : Set β
h✝ : a ∈ s
⊢ ↑↑(↑κ a) t = ↑↑(↑κ a) t
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
t : Set β
h✝ : ¬a ∈ s
⊢ ↑↑(↑η a) t = ↑↑(↑η a) t
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
⊢ IsMarkovKernel (kernel.piecewise hs κ η)
[PROOFSTEP]
refine' ⟨fun a => ⟨_⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
a : α
⊢ ↑↑(↑(kernel.piecewise hs κ η) a) Set.univ = 1
[PROOFSTEP]
rw [piecewise_apply', measure_univ, measure_univ, ite_self]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel (kernel.piecewise hs κ η)
[PROOFSTEP]
refine' ⟨⟨max (IsFiniteKernel.bound κ) (IsFiniteKernel.bound η), _, fun a => _⟩⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ max (IsFiniteKernel.bound κ) (IsFiniteKernel.bound η) < ⊤
[PROOFSTEP]
exact max_lt (IsFiniteKernel.bound_lt_top κ) (IsFiniteKernel.bound_lt_top η)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ↑↑(↑(kernel.piecewise hs κ η) a) Set.univ ≤ max (IsFiniteKernel.bound κ) (IsFiniteKernel.bound η)
[PROOFSTEP]
rw [piecewise_apply']
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (if a ∈ s then ↑↑(↑κ a) Set.univ else ↑↑(↑η a) Set.univ) ≤ max (IsFiniteKernel.bound κ) (IsFiniteKernel.bound η)
[PROOFSTEP]
exact (ite_le_sup _ _ _).trans (sup_le_sup (measure_le_bound _ _ _) (measure_le_bound _ _ _))
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ IsSFiniteKernel (piecewise hs κ η)
[PROOFSTEP]
refine' ⟨⟨fun n => piecewise hs (seq κ n) (seq η n), inferInstance, _⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ piecewise hs κ η = kernel.sum fun n => piecewise hs (seq κ n) (seq η n)
[PROOFSTEP]
ext1 a
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ ↑(piecewise hs κ η) a = ↑(kernel.sum fun n => piecewise hs (seq κ n) (seq η n)) a
[PROOFSTEP]
simp_rw [sum_apply, kernel.piecewise_apply]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ (if a ∈ s then ↑κ a else ↑η a) = Measure.sum fun n => if a ∈ s then ↑(seq κ n) a else ↑(seq η n) a
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
h✝ : a ∈ s
⊢ ↑κ a = Measure.sum fun n => ↑(seq κ n) a
[PROOFSTEP]
exact (measure_sum_seq _ a).symm
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
h✝ : ¬a ∈ s
⊢ ↑η a = Measure.sum fun n => ↑(seq η n) a
[PROOFSTEP]
exact (measure_sum_seq _ a).symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
⊢ ∫⁻ (b : β), g b ∂↑(piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β), g b ∂↑κ a else ∫⁻ (b : β), g b ∂↑η a
[PROOFSTEP]
simp_rw [piecewise_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
⊢ (∫⁻ (b : β), g b ∂if a ∈ s then ↑κ a else ↑η a) = if a ∈ s then ∫⁻ (b : β), g b ∂↑κ a else ∫⁻ (b : β), g b ∂↑η a
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
h✝ : a ∈ s
⊢ ∫⁻ (b : β), g b ∂↑κ a = ∫⁻ (b : β), g b ∂↑κ a
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
h✝ : ¬a ∈ s
⊢ ∫⁻ (b : β), g b ∂↑η a = ∫⁻ (b : β), g b ∂↑η a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
⊢ ∫⁻ (b : β) in t, g b ∂↑(piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β) in t, g b ∂↑κ a else ∫⁻ (b : β) in t, g b ∂↑η a
[PROOFSTEP]
simp_rw [piecewise_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
⊢ (∫⁻ (b : β) in t, g b ∂if a ∈ s then ↑κ a else ↑η a) =
    if a ∈ s then ∫⁻ (b : β) in t, g b ∂↑κ a else ∫⁻ (b : β) in t, g b ∂↑η a
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
h✝ : a ∈ s
⊢ ∫⁻ (b : β) in t, g b ∂↑κ a = ∫⁻ (b : β) in t, g b ∂↑κ a
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
h✝ : ¬a ∈ s
⊢ ∫⁻ (b : β) in t, g b ∂↑η a = ∫⁻ (b : β) in t, g b ∂↑η a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
g : β → E
⊢ ∫ (b : β), g b ∂↑(piecewise hs κ η) a = if a ∈ s then ∫ (b : β), g b ∂↑κ a else ∫ (b : β), g b ∂↑η a
[PROOFSTEP]
simp_rw [piecewise_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
g : β → E
⊢ (∫ (b : β), g b ∂if a ∈ s then ↑κ a else ↑η a) = if a ∈ s then ∫ (b : β), g b ∂↑κ a else ∫ (b : β), g b ∂↑η a
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
g : β → E
h✝ : a ∈ s
⊢ ∫ (b : β), g b ∂↑κ a = ∫ (b : β), g b ∂↑κ a
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
g : β → E
h✝ : ¬a ∈ s
⊢ ∫ (b : β), g b ∂↑η a = ∫ (b : β), g b ∂↑η a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
g : β → E
t : Set β
⊢ ∫ (b : β) in t, g b ∂↑(piecewise hs κ η) a = if a ∈ s then ∫ (b : β) in t, g b ∂↑κ a else ∫ (b : β) in t, g b ∂↑η a
[PROOFSTEP]
simp_rw [piecewise_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
g : β → E
t : Set β
⊢ (∫ (b : β) in t, g b ∂if a ∈ s then ↑κ a else ↑η a) =
    if a ∈ s then ∫ (b : β) in t, g b ∂↑κ a else ∫ (b : β) in t, g b ∂↑η a
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
g : β → E
t : Set β
h✝ : a ∈ s
⊢ ∫ (b : β) in t, g b ∂↑κ a = ∫ (b : β) in t, g b ∂↑κ a
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x => x ∈ s
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
g : β → E
t : Set β
h✝ : ¬a ∈ s
⊢ ∫ (b : β) in t, g b ∂↑η a = ∫ (b : β) in t, g b ∂↑η a
[PROOFSTEP]
rfl
