integral_stieltjesOfMeasurableRat

English

For any a ∈ α and x ∈ ℝ, the integral of stieltjesOfMeasurableRat over all β with respect to ν(a) equals (κ a).real(univ × Iic x).

Русский

Для любых a ∈ α и x ∈ ℝ интеграл от функции stieltlesOfMeasurableRat по всем β с измерением ν(a) равен (κ a).real(univ × Iic x).

LaTeX

$$$\forall a\in\alpha,\; \forall x\in\mathbb{R},\qquad \int_{b} \text{stieltjesOfMeasurableRat}(f, hf.measurable)(a,b,x)\, d(ν a)(b) = (κ a).real(\text{univ} × I_i c x).$$$

Lean4

theorem integral_stieltjesOfMeasurableRat [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ) :
    ∫ b, stieltjesOfMeasurableRat f hf.measurable (a, b) x ∂(ν a) = (κ a).real (univ ×ˢ Iic x) := by
  rw [← setIntegral_univ, setIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.univ]

Похожие утверждения