English
Let ρ be a finite measure on α × ℝ. Then for almost every a with respect to the first marginal ρ_fst, we have that for every rational r, the preCDF ρ r a is bounded above by 1; i.e., preCDF ρ r a ≤ 1 for a.e. a and all r ∈ ℚ.
Русский
Пусть ρ — конечная мера на α × ℝ. Тогда для почти всех a относительно первой маргиалевой меры ρ_fst выполняется, что для любого рационального r функция preCDF ρ r a удовлетворяет неравенству preCDF ρ r a ≤ 1; то есть для почти всех a и для всех r ∈ ℚ выполняется неравенство.
LaTeX
$$$\\\\forall^{\\\\mathrm{a.e.}}\, a \\,\\\\partial ρ_{\\\\mathrm{fst}}, \\\\forall r \\\\in \\\\\\mathbb{Q}, \\\\mathrm{preCDF}(ρ,r,a) \\\\\le 1.$$
Lean4
theorem preCDF_le_one (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] : ∀ᵐ a ∂ρ.fst, ∀ r, preCDF ρ r a ≤ 1 :=
by
rw [ae_all_iff]
refine fun r ↦ ae_le_of_forall_setLIntegral_le_of_sigmaFinite measurable_preCDF fun s hs _ ↦ ?_
rw [setLIntegral_preCDF_fst ρ r hs]
simp only [lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]
exact Measure.IicSnd_le_fst ρ r s
