English
In the rat-case, the lintegral over ν a of ofReal(stieltjesOfMeasurableRat(..., q)) equals κ a on univ ×ˢ Iic(q).
Русский
В случае Rat, линтеграл по ν a от ofReal(stieltles...) равен мере κ a на универсальном множестве × Iic(q).
LaTeX
$$$\\lintegral_{b} \\; ENNReal.ofReal\\bigl(\\text{stieltjesOfMeasurableRat}(f, hf.measurable,(a,b), q)\\bigr) \\, d(ν a) = κ(a)(univ ×ˢ Iic(q)).$$$
Lean4
theorem setLIntegral_stieltjesOfMeasurableRat [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ)
{s : Set β} (hs : MeasurableSet s) :
∫⁻ b in s, ENNReal.ofReal (stieltjesOfMeasurableRat f hf.measurable (a, b) x) ∂(ν a) = κ a (s ×ˢ Iic x) := by
-- We have the result for `x : ℚ` thanks to `setLIntegral_stieltjesOfMeasurableRat_rat`.
-- We use a monotone convergence argument to extend it to the reals.
by_cases hρ_zero : (ν a).restrict s = 0
· rw [hρ_zero, lintegral_zero_measure]
have ⟨q, hq⟩ := exists_rat_gt x
suffices κ a (s ×ˢ Iic (q : ℝ)) = 0 by
symm
refine measure_mono_null (fun p ↦ ?_) this
simp only [mem_prod, mem_Iic, and_imp]
exact fun h1 h2 ↦ ⟨h1, h2.trans hq.le⟩
suffices (κ a).real (s ×ˢ Iic (q : ℝ)) = 0
by
rw [measureReal_eq_zero_iff] at this
simpa [measure_ne_top] using this
rw [← hf.setIntegral a hs q]
simp [hρ_zero]
have h :
∫⁻ b in s, ENNReal.ofReal (stieltjesOfMeasurableRat f hf.measurable (a, b) x) ∂(ν a) =
∫⁻ b in s,
⨅ r : { r' : ℚ // x < r' }, ENNReal.ofReal (stieltjesOfMeasurableRat f hf.measurable (a, b) r) ∂(ν a) :=
by
congr with b : 1
simp_rw [← measure_stieltjesOfMeasurableRat_Iic]
rw [← Monotone.measure_iInter]
· congr with y : 1
simp only [mem_Iic, mem_iInter, Subtype.forall]
refine ⟨fun h a ha ↦ h.trans ?_, fun h ↦ ?_⟩
· exact mod_cast ha.le
· refine le_of_forall_lt_rat_imp_le fun q hq ↦ h q ?_
exact mod_cast hq
· exact fun r r' hrr' ↦ Iic_subset_Iic.mpr <| mod_cast hrr'
· exact fun _ ↦ nullMeasurableSet_Iic
· obtain ⟨q, hq⟩ := exists_rat_gt x
exact ⟨⟨q, hq⟩, measure_ne_top _ _⟩
have h_nonempty : Nonempty { r' : ℚ // x < ↑r' } :=
by
obtain ⟨r, hrx⟩ := exists_rat_gt x
exact ⟨⟨r, hrx⟩⟩
rw [h, lintegral_iInf_directed_of_measurable hρ_zero fun q : { r' : ℚ // x < ↑r' } ↦ ?_]
rotate_left
· intro b
rw [setLIntegral_stieltjesOfMeasurableRat_rat hf a _ hs]
exact measure_ne_top _ _
· refine Monotone.directed_ge fun i j hij b ↦ ?_
simp_rw [← measure_stieltjesOfMeasurableRat_Iic]
refine measure_mono (Iic_subset_Iic.mpr ?_)
exact mod_cast hij
· refine Measurable.ennreal_ofReal ?_
exact (measurable_stieltjesOfMeasurableRat hf.measurable _).comp measurable_prodMk_left
simp_rw [setLIntegral_stieltjesOfMeasurableRat_rat hf _ _ hs]
rw [← Monotone.measure_iInter]
· rw [← prod_iInter]
congr with y
simp only [mem_iInter, mem_Iic, Subtype.forall]
exact ⟨le_of_forall_lt_rat_imp_le, fun hyx q hq ↦ hyx.trans hq.le⟩
· exact fun i j hij ↦ prod_mono_right (by gcongr)
· exact fun i ↦ (hs.prod measurableSet_Iic).nullMeasurableSet
· exact ⟨h_nonempty.some, measure_ne_top _ _⟩
