English
For a finite measure ρ on α × ℝ, the auxiliary object formed by the function (p, r) ↦ (preCDF ρ r p.2)^{toReal}, together with the constant kernels Unit ρ and Unit ρ.fst, constitutes an IsRatCondKernelCDFAux structure. This encodes monotonicity, nonnegativity, and suitable limit behavior required for rational conditioning of the CDF.
Русский
Для конечной меры ρ на α × ℝ соответствующая вспомогательная конструкция, заданная функцией (p, r) ↦ (preCDF ρ r p.2)^{toReal} вместе с константными ядрами Unit ρ и Unit ρ.fst образует структуру IsRatCondKernelCDFAux, обеспечивающую монотонность, неотрицательность и нужное граничное поведение для рационального условного распределения функции распределения.
LaTeX
$$$IsRatCondKernelCDFAux\\left( (p,r) \\mapsto (\\mathrm{preCDF}(ρ,r,p.2))^{\\mathrm{toReal}} \\, , \\, \\mathrm{Kernel.const}\, Unit\\, ρ , \\mathrm{Kernel.const}\, Unit\\, ρ.fst \\right).$$$
Lean4
theorem isRatCondKernelCDFAux_preCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] :
IsRatCondKernelCDFAux (fun p r ↦ (preCDF ρ r p.2).toReal) (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)
where
measurable := measurable_preCDF'.comp measurable_snd
mono' a r r'
hrr' := by
filter_upwards [monotone_preCDF ρ, preCDF_le_one ρ] with a h₁ h₂
exact ENNReal.toReal_mono ((h₂ _).trans_lt ENNReal.one_lt_top).ne (h₁ hrr')
nonneg' _ q := by simp
le_one' a
q := by
simp only [Kernel.const_apply]
filter_upwards [preCDF_le_one ρ] with a ha
refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_
simp [ha]
tendsto_integral_of_antitone a s _
hs_tendsto := by
simp_rw [Kernel.const_apply, integral_preCDF_fst ρ]
have h := ρ.tendsto_IicSnd_atBot MeasurableSet.univ
rw [← ENNReal.toReal_zero]
have h0 : Tendsto ENNReal.toReal (𝓝 0) (𝓝 0) := ENNReal.continuousAt_toReal ENNReal.zero_ne_top
exact h0.comp (h.comp hs_tendsto)
tendsto_integral_of_monotone a s _
hs_tendsto := by
simp_rw [Kernel.const_apply, integral_preCDF_fst ρ]
have h := ρ.tendsto_IicSnd_atTop MeasurableSet.univ
have h0 : Tendsto ENNReal.toReal (𝓝 (ρ.fst univ)) (𝓝 (ρ.fst.real univ)) :=
ENNReal.continuousAt_toReal (measure_ne_top _ _)
exact h0.comp (h.comp hs_tendsto)
integrable _ q := integrable_preCDF ρ q
setIntegral a s hs
q := by
rw [Kernel.const_apply, Kernel.const_apply, setIntegral_preCDF_fst _ _ hs, measureReal_def, measureReal_def,
Measure.IicSnd_apply _ _ hs]
