English
For a ≤ b, the conditional expectation of a trajectory functional f given the σ-algebra generated by the first b steps equals the conditional expectation of f with the trajectory restricted to those steps, computed along traj κ a x0.
Русский
Для a ≤ b условное ожидание функционала траектории по системе σ, порождаемой первыми b шагами, эквивалентно условному ожиданию f на траектории κ a x0 с ограничением по этим шагам.
LaTeX
$$$\\operatorname{condExp}_{\\pi_LE^b} (f, \\operatorname{traj}_κ a x_0) = \\operatorname{traj}_κ a x_0[f]$$$
Lean4
theorem condExp_traj {a b : ℕ} (hab : a ≤ b) {x₀ : Π i : Iic a, X i} {f : (Π n, X n) → E}
(i_f : Integrable f (traj κ a x₀)) :
(traj κ a x₀)[f|piLE b] =ᵐ[traj κ a x₀] fun x ↦ ∫ y, f y ∂traj κ b (frestrictLe b x) :=
by
have i_f' : Integrable (fun x ↦ ∫ y, f y ∂(traj κ b) x) (((traj κ a) x₀).map (frestrictLe b)) :=
by
rw [← map_apply _ (measurable_frestrictLe _), traj_map_frestrictLe _ _]
rw [← traj_comp_partialTraj hab] at i_f
exact i_f.integral_comp
refine
ae_eq_condExp_of_forall_setIntegral_eq (piLE.le _) i_f
(fun s _ _ ↦ i_f'.comp_aemeasurable (measurable_frestrictLe b).aemeasurable |>.integrableOn) ?_ ?_ |>.symm <;>
rw [piLE_eq_comap_frestrictLe]
· rintro - ⟨t, mt, rfl⟩ -
simp_rw [Function.comp_apply]
rw [← setIntegral_map mt i_f'.1, ← map_apply, traj_map_frestrictLe, setIntegral_traj_partialTraj hab i_f mt]
all_goals fun_prop
· exact (i_f'.1.comp_ae_measurable' (measurable_frestrictLe b).aemeasurable)
