setLIntegral_preCDF_fst — Mathlib

English

SetLIntegral equality with preCDF for rational cast r.cast.

Русский

Эквивалентность SetLIntegral preCDF fst для r.cast.

LaTeX

$$$\int^{\llbracket x \rrbracket}_{x \in s} preCDF ρ r x \partial ρ.fst = ρ.IicSnd r cast\ s$$$

Lean4

theorem setLIntegral_preCDF_fst (ρ : Measure (α × ℝ)) (r : ℚ) {s : Set α} (hs : MeasurableSet s) [IsFiniteMeasure ρ] :
    ∫⁻ x in s, preCDF ρ r x ∂ρ.fst = ρ.IicSnd r s :=
  by
  have : ∀ r, ∫⁻ x in s, preCDF ρ r x ∂ρ.fst = ∫⁻ x in s, (preCDF ρ r * 1) x ∂ρ.fst := by
    simp only [mul_one, forall_const]
  rw [this, ← setLIntegral_withDensity_eq_setLIntegral_mul _ measurable_preCDF _ hs]
  ·
    simp only [withDensity_preCDF ρ r, Pi.one_apply, lintegral_one, Measure.restrict_apply, MeasurableSet.univ,
      univ_inter]
  · rw [Pi.one_def]
    exact measurable_const

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