English
If κ ≤ κ', ν ≤ ν', then densityProcess(ν') ≤ densityProcess(ν) pointwise.
Русский
Если ядра κ≤κ', ν≤ν', то densityProcess(ν') ≤ densityProcess(ν) по каждому аргументу.
LaTeX
$$$\text{densityProcess}(ν',n,a,x,s) \le \text{densityProcess}(ν,n,a,x,s)$$$
Lean4
theorem condExp_densityProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν] {i j : ℕ} (hij : i ≤ j) (a : α) {s : Set β}
(hs : MeasurableSet s) :
(ν a)[fun x ↦ densityProcess κ ν j a x s|countableFiltration γ i] =ᵐ[ν a] fun x ↦ densityProcess κ ν i a x s :=
by
refine (ae_eq_condExp_of_forall_setIntegral_eq ?_ ?_ ?_ ?_ ?_).symm
· exact integrable_densityProcess hκν j a hs
· exact fun _ _ _ ↦ (integrable_densityProcess hκν _ _ hs).integrableOn
· intro x hx _
rw [setIntegral_densityProcess hκν i a hs hx, setIntegral_densityProcess_of_le hκν hij a hs hx]
· exact StronglyMeasurable.aestronglyMeasurable (stronglyMeasurable_countableFiltration_densityProcess κ ν i a hs)
