English
The density along Iic intervals defines a Rat-conditional kernel CDF with respect to κ: density κ (fst κ) p.1 p.2 (Iic q) yields an isRatCondKernelCDF.
Русский
Плотность по интервалам Iic образует рациональную условную функцию распределения по отношению к κ: density κ (fst κ) p.1 p.2 (Iic q) образует IsRatCondKernelCDF.
LaTeX
$$$IsRatCondKernelCDF\left( (p,q) \mapsto \kappa.density (\kappa.fst) p.1 p.2 (Iic q) \right) \kappa (\kappa.fst)$$$
Lean4
theorem isRatCondKernelCDFAux_density_Iic (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] :
IsRatCondKernelCDFAux (fun (p : α × γ) q ↦ density κ (fst κ) p.1 p.2 (Iic q)) κ (fst κ)
where
measurable := measurable_pi_iff.mpr fun _ ↦ measurable_density κ (fst κ) measurableSet_Iic
mono' a q r hqr := ae_of_all _ fun c ↦ density_mono_set le_rfl a c (Iic_subset_Iic.mpr (by exact_mod_cast hqr))
nonneg' _ _ := ae_of_all _ fun _ ↦ density_nonneg le_rfl _ _ _
le_one' _ _ := ae_of_all _ fun _ ↦ density_le_one le_rfl _ _ _
tendsto_integral_of_antitone a s hs_anti
hs_tendsto := by
let s' : ℕ → Set ℝ := fun n ↦ Iic (s n)
refine tendsto_integral_density_of_antitone le_rfl a s' ?_ ?_ (fun _ ↦ measurableSet_Iic)
· refine fun i j hij ↦ Iic_subset_Iic.mpr ?_
exact mod_cast hs_anti hij
· ext x
simp only [mem_iInter, mem_Iic, mem_empty_iff_false, iff_false, not_forall, not_le, s']
rw [tendsto_atTop_atBot] at hs_tendsto
have ⟨q, hq⟩ := exists_rat_lt x
obtain ⟨i, hi⟩ := hs_tendsto q
refine ⟨i, lt_of_le_of_lt ?_ hq⟩
exact mod_cast hi i le_rfl
tendsto_integral_of_monotone a s hs_mono
hs_tendsto := by
rw [fst_real_apply _ _ MeasurableSet.univ]
let s' : ℕ → Set ℝ := fun n ↦ Iic (s n)
refine tendsto_integral_density_of_monotone (le_rfl : fst κ ≤ fst κ) a s' ?_ ?_ (fun _ ↦ measurableSet_Iic)
· exact fun i j hij ↦ Iic_subset_Iic.mpr (by exact mod_cast hs_mono hij)
· ext x
simp only [mem_iUnion, mem_univ, iff_true]
rw [tendsto_atTop_atTop] at hs_tendsto
have ⟨q, hq⟩ := exists_rat_gt x
obtain ⟨i, hi⟩ := hs_tendsto q
refine ⟨i, hq.le.trans ?_⟩
exact mod_cast hi i le_rfl
integrable a _ := integrable_density le_rfl a measurableSet_Iic
setIntegral a _ hA _ := setIntegral_density le_rfl a measurableSet_Iic hA
