[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ : { x // x ∈ kernel α β }
⊢ Measure.bind (μ + ν) ↑κ = Measure.bind μ ↑κ + Measure.bind ν ↑κ
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ : { x // x ∈ kernel α β }
s : Set β
hs : MeasurableSet s
⊢ ↑↑(Measure.bind (μ + ν) ↑κ) s = ↑↑(Measure.bind μ ↑κ + Measure.bind ν ↑κ) s
[PROOFSTEP]
rw [Measure.bind_apply hs (kernel.measurable _), lintegral_add_measure, Measure.coe_add, Pi.add_apply,
  Measure.bind_apply hs (kernel.measurable _), Measure.bind_apply hs (kernel.measurable _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
μ : Measure α
r : ℝ≥0∞
⊢ Measure.bind (r • μ) ↑κ = r • Measure.bind μ ↑κ
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
μ : Measure α
r : ℝ≥0∞
s : Set β
hs : MeasurableSet s
⊢ ↑↑(Measure.bind (r • μ) ↑κ) s = ↑↑(r • Measure.bind μ ↑κ) s
[PROOFSTEP]
rw [Measure.bind_apply hs (kernel.measurable _), lintegral_smul_measure, Measure.coe_smul, Pi.smul_apply,
  Measure.bind_apply hs (kernel.measurable _), smul_eq_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
μ : Measure α
⊢ const α (Measure.bind μ ↑κ) = κ ∘ₖ const α μ
[PROOFSTEP]
ext a s hs
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
μ : Measure α
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(const α (Measure.bind μ ↑κ)) a) s = ↑↑(↑(κ ∘ₖ const α μ) a) s
[PROOFSTEP]
simp_rw [comp_apply' _ _ _ hs, const_apply, Measure.bind_apply hs (kernel.measurable _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
μ : Measure α
a : α
⊢ ↑(κ ∘ₖ const α μ) a = Measure.bind μ ↑κ
[PROOFSTEP]
rw [← const_apply (μ.bind κ) a, const_bind_eq_comp_const κ μ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : { x // x ∈ kernel α α }
μ : Measure α
hκ : Invariant κ μ
⊢ κ ∘ₖ const α μ = const α μ
[PROOFSTEP]
rw [← const_bind_eq_comp_const κ μ, hκ.def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : { x // x ∈ kernel α α }
μ : Measure α
inst✝ : IsSFiniteKernel κ
hκ : Invariant κ μ
hη : Invariant η μ
⊢ Invariant (κ ∘ₖ η) μ
[PROOFSTEP]
cases' isEmpty_or_nonempty α with _ hα
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : { x // x ∈ kernel α α }
μ : Measure α
inst✝ : IsSFiniteKernel κ
hκ : Invariant κ μ
hη : Invariant η μ
h✝ : IsEmpty α
⊢ Invariant (κ ∘ₖ η) μ
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : { x // x ∈ kernel α α }
μ : Measure α
inst✝ : IsSFiniteKernel κ
hκ : Invariant κ μ
hη : Invariant η μ
hα : Nonempty α
⊢ Invariant (κ ∘ₖ η) μ
[PROOFSTEP]
simp_rw [Invariant, ← comp_const_apply_eq_bind (κ ∘ₖ η) μ hα.some, comp_assoc, hη.comp_const, hκ.comp_const,
  const_apply]
