English
Let ρ be a finite measure on α × ℝ and r be rational. For any measurable set s ⊆ α, the integral of the real valued preCDF over s with respect to ρ_fst equals the real measure of s under ρ restricted to s × (-∞, r]. Equivalently, ∫_{a∈s} (preCDF ρ r a)^{toReal} dρ.fst = (ρ.IicSnd r.cast)^{real}(s).
Русский
Пусть ρ — конечная мера на α × ℝ и r рационально. Для любого измеримого множества s ⊆ α интеграл действительного значения preCDF по s по мере ρ_fst равен вещественной мере множества s, ограниченного сверху (-∞, r], по мере ρ, ограниченной на s × (-∞, r]. Иными словами, ∫_{a∈s} (preCDF ρ r a)^{toReal} dρ.fst = (ρ.IicSnd r.cast)^{real}(s).
LaTeX
$$$\\int_{a \in s} (\\mathrm{preCDF}(ρ,r,a))^{\\mathrm{toReal}} dρ_{\\\\mathrm{fst}}(a) = (ρ.IicSnd(r.cast))^{\\mathrm{real}}(s).$$
Lean4
theorem setIntegral_preCDF_fst (ρ : Measure (α × ℝ)) (r : ℚ) {s : Set α} (hs : MeasurableSet s) [IsFiniteMeasure ρ] :
∫ x in s, (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd r).real s :=
by
rw [integral_toReal]
· rw [setLIntegral_preCDF_fst _ _ hs, measureReal_def]
· exact measurable_preCDF.aemeasurable
· refine ae_restrict_of_ae ?_
filter_upwards [preCDF_le_one ρ] with a ha
exact (ha r).trans_lt ENNReal.one_lt_top
