English
IicSnd r is absolutely continuous with respect to fst.
Русский
IicSnd r абсолютно непрерывна по отношению к fst.
LaTeX
$$$IicSnd_{\rho} (r) \ll \rho.fst$$$
Lean4
theorem setLIntegral_toKernel_prod [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν) (a : α) {s : Set β}
(hs : MeasurableSet s) {t : Set ℝ} (ht : MeasurableSet t) :
∫⁻ b in s, hf.toKernel f (a, b) t ∂(ν a) = κ a (s ×ˢ t) := by
-- `setLIntegral_toKernel_Iic` gives the result for `t = Iic x`. These sets form a
-- π-system that generates the Borel σ-algebra, hence we can get the same equality for any
-- measurable set `t`.
induction t, ht using MeasurableSpace.induction_on_inter (borel_eq_generateFrom_Iic ℝ) isPiSystem_Iic with
| empty => simp only [measure_empty, lintegral_const, zero_mul, prod_empty]
| basic t ht =>
obtain ⟨q, rfl⟩ := ht
exact setLIntegral_toKernel_Iic hf a _ hs
| compl t ht iht =>
calc
∫⁻ b in s, hf.toKernel f (a, b) tᶜ ∂(ν a) =
∫⁻ b in s, hf.toKernel f (a, b) univ - hf.toKernel f (a, b) t ∂(ν a) :=
by congr with x; rw [measure_compl ht (measure_ne_top (hf.toKernel f (a, x)) _)]
_ = ∫⁻ b in s, hf.toKernel f (a, b) univ ∂(ν a) - ∫⁻ b in s, hf.toKernel f (a, b) t ∂(ν a) :=
by
rw [lintegral_sub]
· exact (Kernel.measurable_coe (hf.toKernel f) ht).comp measurable_prodMk_left
· rw [iht]
exact measure_ne_top _ _
· exact Eventually.of_forall fun a ↦ measure_mono (subset_univ _)
_ = κ a (s ×ˢ univ) - κ a (s ×ˢ t) := by rw [setLIntegral_toKernel_univ hf a hs, iht]
_ = κ a (s ×ˢ tᶜ) :=
by
rw [← measure_diff _ (hs.prod ht).nullMeasurableSet (measure_ne_top _ _)]
· rw [prod_diff_prod, compl_eq_univ_diff]
simp only [diff_self, empty_prod, union_empty]
· rw [prod_subset_prod_iff]
exact Or.inl ⟨subset_rfl, subset_univ t⟩
| iUnion f hf_disj hf_meas ihf =>
simp_rw [measure_iUnion hf_disj hf_meas]
rw [lintegral_tsum, prod_iUnion, measure_iUnion]
· simp_rw [ihf]
· exact hf_disj.mono fun i j h ↦ h.set_prod_right _ _
· exact fun i ↦ MeasurableSet.prod hs (hf_meas i)
· exact fun i ↦ ((Kernel.measurable_coe _ (hf_meas i)).comp measurable_prodMk_left).aemeasurable.restrict
