English
If f is AEStronglyMeasurable with respect to traj κ a x0, then the lintegral of f along traj κ a x0 equals the lintegral of f after updating x via updateFinset, for every a.
Русский
Если f AEStronglyMeasurable относительно traj κ a x0, то линтеграл по траектории равен линтегралу после обновления x через updateFinset, для каждого a.
LaTeX
$$$\\text{If } f \\text{ is AEStronglyMeasurable w.r.t. } \\operatorname{traj}_κ a x_0, \\int f \\, d\\operatorname{traj}_κ a x_0 = \\int f(\\operatorname{updateFinset}(x, \\mathsf{Iic}\\,a) x) \\, d\\operatorname{traj}_κ a x_0$$$
Lean4
theorem condExp_traj' {a b c : ℕ} (hab : a ≤ b) (hbc : b ≤ c) (x₀ : Π i : Iic a, X i) (f : (Π n, X n) → E) :
(traj κ a x₀)[f|piLE b] =ᵐ[traj κ a x₀] fun x ↦
∫ y, ((traj κ a x₀)[f|piLE c]) (updateFinset x (Iic c) y) ∂partialTraj κ b c (frestrictLe b x) :=
by
have i_cf : Integrable ((traj κ a x₀)[f|piLE c]) (traj κ a x₀) := integrable_condExp
have mcf : StronglyMeasurable ((traj κ a x₀)[f|piLE c]) := stronglyMeasurable_condExp.mono (piLE.le c)
filter_upwards [piLE.condExp_condExp f hbc, condExp_traj hab i_cf] with x h1 h2
rw [← h1, h2, ← traj_map_frestrictLe, Kernel.map_apply, integral_map]
· congr with y
apply stronglyMeasurable_condExp.dependsOn_of_piLE
simp only [Set.mem_Iic, updateFinset, mem_Iic, frestrictLe_apply, dite_eq_ite]
exact fun i hi ↦ (if_pos hi).symm
any_goals fun_prop
exact (mcf.comp_measurable measurable_updateFinset).aestronglyMeasurable
