English
The partial trajectory up to a combined with the full trajectory from b forms a joint kernel that corresponds to the pair (frestrictLe b x, x). This is a product-like decomposition at the level of kernels.
Русский
Частичная траектория до a вместе с полной траекторией до b образуют совместное ядро, соответствующее пары (frestrictLe b x, x). Это разложение ядер в виде произведения.
LaTeX
$$$\\,(\\partial_\\kappa a b u) \\otimes_\\mu (\\operatorname{traj}_κ b) = (\\operatorname{traj}_κ a u).map(\\lambda x. (\\operatorname{frestrictLe} b x, x))$$$
Lean4
theorem partialTraj_compProd_traj {a b : ℕ} (hab : a ≤ b) (u : Π i : Iic a, X i) :
(partialTraj κ a b u) ⊗ₘ (traj κ b) = (traj κ a u).map (fun x ↦ (frestrictLe b x, x)) :=
by
ext s ms
rw [Measure.map_apply, Measure.compProd_apply, ← traj_comp_partialTraj hab, comp_apply']
· congr 1 with x
rw [← traj_map_updateFinset, Measure.map_apply, Measure.map_apply]
· congr 1 with y
simp only [Set.mem_preimage]
congrm (fun i ↦ ?_, fun i ↦ ?_) ∈ s <;> simp [updateFinset]
any_goals fun_prop
all_goals exact ms.preimage (by fun_prop)
any_goals exact ms.preimage (by fun_prop)
fun_prop
