-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma setLIntegral_stieltjesOfMeasurableRat_rat [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν)
    (a : α) (q : ℚ) {s : Set β} (hs : MeasurableSet s) :
    ∫⁻ b in s, ENNReal.ofReal (stieltjesOfMeasurableRat f hf.measurable (a, b) q) ∂(ν a)
      = κ a (s ×ˢ Iic (q : ℝ))

Proof state:
case hfi
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun b => f (a, b) q) (ν a)

Tactic:
exact hf.integrable a q

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ ENNReal.ofReal (∫ (x : β) in s, ↑(stieltjesOfMeasurableRat f ⋯ (a, x)) ↑q ∂ν a) = (κ a) (s ×ˢ Iic ↑q)

Tactic:
rw [setIntegral_stieltjesOfMeasurableRat_rat hf a q hs, ENNReal.ofReal_toReal]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ (κ a) (s ×ˢ Iic ↑q) ≠ ⊤

Proof state:
case hfi
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) ((ν a).restrict s)

Tactic:
refine Integrable.restrict ?_

Result:
case hfi
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) (ν a)

Proof state:
case hfi
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) (ν a)

Tactic:
rw [integrable_congr (stieltjesOfMeasurableRat_ae_eq hf a q)]

Result:
case hfi
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun b => f (a, b) q) (ν a)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ (κ a) (s ×ˢ Iic ↑q) ≠ ⊤

Tactic:
exact measure_ne_top _ _

Result:
no goals

Proof state:
case f_nn
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ 0 ≤ᶠ[ae ((ν a).restrict s)] fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q

Tactic:
exact ae_of_all _ (fun x ↦ stieltjesOfMeasurableRat_nonneg _ _ _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) ∂ν a = (κ a) (s ×ˢ Iic ↑q)

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ ENNReal.ofReal (∫ (x : β) in s, ↑(stieltjesOfMeasurableRat f ⋯ (a, x)) ↑q ∂ν a) = (κ a) (s ×ˢ Iic ↑q)

case hfi
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) ((ν a).restrict s)

case f_nn
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ 0 ≤ᶠ[ae ((ν a).restrict s)] fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q