English
If f depends only on coordinates up to a, then lmarginalPartialTraj κ b c f equals f after projecting to the left-hand side up to a, provided a ≤ b ≤ c.
Русский
Если f зависит только от координат до a, тогда lmarginalPartialTraj κ b c f равна f после проекции на левую часть до a, при условии a ≤ b ≤ c.
LaTeX
$$$ lmarginalPartialTraj\,κ\,b\,c\;f = f \quad \text{if } f\text{ depends on } Iic a \text{ and } a \le b \le c$$$
Lean4
/-- If `f` only depends on the variables up to rank `a` and `a ≤ b`, integrating `f` against
`partialTraj κ b c` does nothing. -/
theorem lmarginalPartialTraj_of_le [∀ n, IsMarkovKernel (κ n)] (c : ℕ) {f : (Π n, X n) → ℝ≥0∞} (mf : Measurable f)
(hf : DependsOn f (Iic a)) (hab : a ≤ b) : lmarginalPartialTraj κ b c f = f :=
by
ext x
rw [lmarginalPartialTraj_eq_lintegral_map mf]
refine @lintegral_eq_const _ _ _ ?_ _ _ (ae_of_all _ fun y ↦ hf fun i hi ↦ ?_)
· refine @IsMarkovKernel.isProbabilityMeasure _ _ _ _ _ ?_ _
exact IsMarkovKernel.map _ (by fun_prop)
· simp_all only [coe_Iic, Set.mem_Iic, Function.updateFinset, mem_Ioc, dite_eq_right_iff]
cutsat
