English
Let κ be a finite kernel on α with a conditional distribution given by f, and let ν be the marginal kernel on α→β. For every a ∈ α, every x ∈ ℝ, and every measurable set s ⊆ β, the integral of the Stieltjes transform over s with respect to ν(a) equals the real-valued measure κ(a) on the product s × (−∞, x]. In symbols, for all a, x and measurable s, ∫_{b∈s} Stieltjes_f(a,b;x) d(ν a)(b) = (κ a).real(s × Iic x).
Русский
Пусть κ — конечный ядро с условным распределением, задаваемым f, а ν — соответствующее маргинальное ядро на α→β. Для любого a ∈ α, любого x ∈ ℝ и любого измеримого множества s ⊆ β выполняется формула: интеграл по b в s от Stieltjes_f(a,b;x) по мере ν(a) равен вещественной мере κ(a) на множество s × (−∞, x]. Обозначения: ∫_{b∈s} Stieltjes_f(a,b;x) d(ν a)(b) = (κ a).real(s × Iic x).
LaTeX
$$$\forall a\in\alpha,\; \forall x\in\mathbb{R},\; \forall s\subseteq \beta\text{ measurable},\qquad \int_{b\in s} \text{stieltjesOfMeasurableRat}(f, hf.measurable)(a,b,x)\, d(\nu a)(b) = (\kappa a).\operatorname{real}(s \times I_i c x).$$$
Lean4
theorem setIntegral_stieltjesOfMeasurableRat [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ)
{s : Set β} (hs : MeasurableSet s) :
∫ b in s, stieltjesOfMeasurableRat f hf.measurable (a, b) x ∂(ν a) = (κ a).real (s ×ˢ Iic x) :=
by
rw [← ENNReal.ofReal_eq_ofReal_iff, ofReal_measureReal]
rotate_left
· exact setIntegral_nonneg hs (fun _ _ ↦ stieltjesOfMeasurableRat_nonneg _ _ _)
· exact ENNReal.toReal_nonneg
rw [ofReal_integral_eq_lintegral_ofReal, setLIntegral_stieltjesOfMeasurableRat hf _ _ hs]
· exact (integrable_stieltjesOfMeasurableRat hf _ _).restrict
· exact ae_of_all _ (fun _ ↦ stieltjesOfMeasurableRat_nonneg _ _ _)
