English
For ρ a finite measure on α × ℝ and any rational x, the function a ↦ (preCDF ρ x a)^{toReal} is integrable with respect to ρ_fst.
Русский
Пусть ρ — конечная мера на α × ℝ и для любого рационального x функция a ↦ (preCDF ρ x a)^{toReal} является интегрируемой по мере ρ_fst.
LaTeX
$$$\\forall x \\in \\mathbb{Q},\\quad \\mathrm{Integrable}_{ρ_{\\\\mathrm fst}}(a \\mapsto (\\mathrm{preCDF}(ρ,x,a))^{\\mathrm{toReal}}).$$$
Lean4
theorem integrable_preCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (x : ℚ) :
Integrable (fun a ↦ (preCDF ρ x a).toReal) ρ.fst :=
by
refine integrable_of_forall_fin_meas_le _ (measure_lt_top ρ.fst univ) ?_ fun t _ _ ↦ ?_
· exact measurable_preCDF.ennreal_toReal.aestronglyMeasurable
· simp_rw [← ofReal_norm_eq_enorm, Real.norm_of_nonneg ENNReal.toReal_nonneg]
rw [← lintegral_one]
refine (setLIntegral_le_lintegral _ _).trans (lintegral_mono_ae ?_)
filter_upwards [preCDF_le_one ρ] with a ha using ENNReal.ofReal_toReal_le.trans (ha _)
