English
For any a, the IicSnd measure on univ equals the restriction to univ × Iic, i.e., the IicSnd coincides with the pushforward of ρ on the universal domain.
Русский
Для любого a мера IicSnd на универсальном множестве совпадает с ограничением на univ × Iic, т.е. IicSnd совпадает с проецируемой мерой ρ на все пространство.
LaTeX
$$$\rho.IicSnd\, r\,\mathrm{univ} = \rho\left(\mathrm{univ} \times Iic\, r\right)$$$
Lean4
theorem setLIntegral_toKernel_univ [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν) (a : α) {s : Set β}
(hs : MeasurableSet s) : ∫⁻ b in s, hf.toKernel f (a, b) univ ∂(ν a) = κ a (s ×ˢ univ) :=
by
rw [← Real.iUnion_Iic_rat, prod_iUnion]
have h_dir : Directed (fun x y ↦ x ⊆ y) fun q : ℚ ↦ Iic (q : ℝ) :=
by
refine Monotone.directed_le fun r r' hrr' ↦ Iic_subset_Iic.mpr ?_
exact mod_cast hrr'
have h_dir_prod : Directed (fun x y ↦ x ⊆ y) fun q : ℚ ↦ s ×ˢ Iic (q : ℝ) :=
by
refine Monotone.directed_le fun i j hij ↦ ?_
refine prod_subset_prod_iff.mpr (Or.inl ⟨subset_rfl, Iic_subset_Iic.mpr ?_⟩)
exact mod_cast hij
simp_rw [h_dir.measure_iUnion, h_dir_prod.measure_iUnion]
rw [lintegral_iSup_directed]
· simp_rw [setLIntegral_toKernel_Iic hf _ _ hs]
· refine fun q ↦ Measurable.aemeasurable ?_
exact (Kernel.measurable_coe _ measurableSet_Iic).comp measurable_prodMk_left
· refine Monotone.directed_le fun i j hij t ↦ measure_mono (Iic_subset_Iic.mpr ?_)
exact mod_cast hij
