-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma setLIntegral_toKernel_prod [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν)
    (a : α) {s : Set β} (hs : MeasurableSet s) {t : Set ℝ} (ht : MeasurableSet t) :
    ∫⁻ b in s, hf.toKernel f (a, b) t ∂(ν a) = κ a (s ×ˢ t)

Proof state:
case basic.intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
q : ℝ
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (Iic q) ∂ν a = (κ a) (s ×ˢ Iic q)

Tactic:
exact setLIntegral_toKernel_Iic hf a _ hs

Result:
no goals

Proof state:
case basic
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : t ∈ range Iic
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)

Tactic:
obtain ⟨q, rfl⟩ := ht

Result:
case basic.intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
q : ℝ
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (Iic q) ∂ν a = (κ a) (s ×ˢ Iic q)

Proof state:
case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ Measurable fun b => ((IsCondKernelCDF.toKernel f hf) (a, b)) t

Tactic:
exact (Kernel.measurable_coe (hf.toKernel f) ht).comp measurable_prod_mk_left

Result:
no goals

Proof state:
case hg_fin
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ (κ a) (s ×ˢ t) ≠ ⊤

Tactic:
exact measure_ne_top _ _

Result:
no goals

Proof state:
case h_le
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ (fun b => ((IsCondKernelCDF.toKernel f hf) (a, b)) t) ≤ᶠ[ae ((ν a).restrict s)] fun b =>
    ((IsCondKernelCDF.toKernel f hf) (a, b)) univ

Tactic:
exact Eventually.of_forall fun a ↦ measure_mono (subset_univ _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ s ⊆ s ∧ t ⊆ univ ∨ s = ∅ ∨ t = ∅

Tactic:
exact Or.inl ⟨subset_rfl, subset_univ t⟩

Result:
no goals

Proof state:
case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∑' (i : ℕ), ∫⁻ (a_1 : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, a_1)) (f i) ∂ν a = ∑' (i : ℕ), (κ a) (s ×ˢ f i)

Tactic:
simp_rw [ihf]

Result:
no goals