monotone_preCDF — Mathlib

English

For almost every a, the function r ↦ preCDF ρ r a is monotone in r.

Русский

Поскольку почти для каждого a функция r ↦ preCDF ρ r a монотонна по r.

LaTeX

$$$\forall^{\mathrm{ae}} a\;\; Monotone\;\left(\lambda r. preCDF ρ r a\right)$$$

Lean4

theorem monotone_preCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] : ∀ᵐ a ∂ρ.fst, Monotone fun r ↦ preCDF ρ r a :=
  by
  simp_rw [Monotone, ae_all_iff]
  refine fun r r' hrr' ↦ ae_le_of_forall_setLIntegral_le_of_sigmaFinite measurable_preCDF fun s hs _ ↦ ?_
  rw [setLIntegral_preCDF_fst ρ r hs, setLIntegral_preCDF_fst ρ r' hs]
  exact Measure.IicSnd_mono ρ (mod_cast hrr') s

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