integrable_densityProcess — Mathlib

English

Under a partial order of kernels, the conditional expectation equality holds a.e. for condExp of densityProcess across a filtration sequence.

Русский

При частичном порядке ядер выполнено равенство почти наверное для condExp плотности через последовательность фильтраций.

LaTeX

$$$\mathsf{ae}\big( \text{kernel}_{ν a} \text{, densityProcess}(ν, j) \big) =\!\! \text{densityProcess}(ν,i) \; a.e.$$$

Lean4

theorem integrable_densityProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (n : ℕ) (a : α) {s : Set β}
    (hs : MeasurableSet s) : Integrable (fun x ↦ densityProcess κ ν n a x s) (ν a) :=
  by
  rw [← memLp_one_iff_integrable]
  refine ⟨Measurable.aestronglyMeasurable ?_, ?_⟩
  · exact measurable_densityProcess_right κ ν n a hs
  · exact (eLpNorm_densityProcess_le hκν n a s).trans_lt (measure_lt_top _ _)

Похожие утверждения