integral_preCDF_fst — Mathlib

English

Let ρ be a finite measure on α × ℝ and r rational. Then the integral of (preCDF ρ r a)^{toReal} over the whole α with respect to ρ_fst equals the real part of ρ(IicSnd r.cast) over univ, i.e., (ρ.IicSnd r.cast).real univ.

Русский

Пусть ρ — конечная мера на α × ℝ и r рационально. Тогда интеграл по всей α функции (preCDF ρ r a)^{toReal} по мере ρ_fst равен вещественной мере множества (-∞, r] в пространстве α × ℝ, то есть (ρ.IicSnd r.cast).real univ.

LaTeX

$$$\\int_{a} (\\mathrm{preCDF}(ρ,r,a))^{\\mathrm{toReal}} dρ_{\\\\mathrm fst}(a) = (ρ.IicSnd(r.cast)).real(\\\\mathrm{univ}).$$

Lean4

theorem integral_preCDF_fst (ρ : Measure (α × ℝ)) (r : ℚ) [IsFiniteMeasure ρ] :
    ∫ x, (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd r).real univ := by
  rw [← setIntegral_univ, setIntegral_preCDF_fst ρ _ MeasurableSet.univ]

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