English
If f depends only on variables up to b, then lmarginalPartialTraj κ a b f is a function depending only on variables up to a (and conversely with symmetry). This captures a kind of locality of dependence.
Русский
Если f зависит только от переменных до b, то lmarginalPartialTraj κ a b f зависит только от переменных до a (и наоборот в симметричном виде). Это отражает локальность зависимости.
LaTeX
$$$ \text{DependsOn}(lmarginalPartialTraj\,κ\,a\,b\;f)\; \text{on } Iic a$$$
Lean4
/-- If `f` only depends on variables up to rank `b`, its integral from `a` to `b` only depends on
variables up to rank `a`. -/
theorem dependsOn_lmarginalPartialTraj [∀ n, IsSFiniteKernel (κ n)] (a : ℕ) {f : (Π n, X n) → ℝ≥0∞}
(hf : DependsOn f (Iic b)) (mf : Measurable f) : DependsOn (lmarginalPartialTraj κ a b f) (Iic a) :=
by
intro x y hxy
obtain hba | hab := le_total b a
· rw [Kernel.lmarginalPartialTraj_le κ hba mf]
exact hf fun i hi ↦ hxy i (Iic_subset_Iic.2 hba hi)
rw [lmarginalPartialTraj_eq_lintegral_map mf, lmarginalPartialTraj_eq_lintegral_map mf]
congrm ∫⁻ z : _, ?_ ∂(partialTraj κ a b).map _ (fun i ↦ ?_)
· exact hxy i.1 i.2
· refine hf.updateFinset _ ?_
rwa [← coe_sdiff, Iic_diff_Ioc_self_of_le hab]
