lintegral_preCDF_fst — Mathlib

English

The Lintegral of preCDF over ρ.fst equals IicSnd evaluated at univ.

Русский

Линтеграл по preCDF над ρ.fst равен IicSnd на univ.

LaTeX

$$$\int^{\infty}_{x} preCDF ρ r x \partial ρ.fst = ρ.IicSnd r univ$$$

Lean4

theorem lintegral_preCDF_fst (ρ : Measure (α × ℝ)) (r : ℚ) [IsFiniteMeasure ρ] :
    ∫⁻ x, preCDF ρ r x ∂ρ.fst = ρ.IicSnd r univ := by
  rw [← setLIntegral_univ, setLIntegral_preCDF_fst ρ r MeasurableSet.univ]

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