English
If each kernel κ_n is Markov and the base f is measurable, then lmarginalPartialTraj κ a b f is a measurable function of the initial data.
Русский
Если каждое ядро κ_n марковское и основание f измеримо, то lmarginalPartialTraj κ a b f — измеримая функция от начальных данных.
LaTeX
$$$ \text{Measurable}(lmarginalPartialTraj\,κ\,a\,b\;f) $$$
Lean4
/-- Integrating `f` against `partialTraj κ a (a + 1)` is the same as integrating against `κ a`. -/
theorem lmarginalPartialTraj_succ [∀ n, IsSFiniteKernel (κ n)] (a : ℕ) {f : (Π n, X n) → ℝ≥0∞} (mf : Measurable f)
(x₀ : Π n, X n) :
lmarginalPartialTraj κ a (a + 1) f x₀ = ∫⁻ x : X (a + 1), f (update x₀ _ x) ∂κ a (frestrictLe a x₀) :=
by
rw [lmarginalPartialTraj, partialTraj_succ_self, lintegral_map, lintegral_id_prod, lintegral_map]
· congrm ∫⁻ x, f (fun i ↦ ?_) ∂_
simp only [updateFinset, mem_Iic, IicProdIoc_def, frestrictLe_apply, piSingleton, MeasurableEquiv.coe_mk,
Equiv.coe_fn_mk, update]
split_ifs with h1 h2 h3 <;> try rfl
all_goals cutsat
all_goals fun_prop
