partialTraj_le — Mathlib

English

If a ≤ b, then partialTraj κ a (b+1) equals the composition of the identity on the left part with the k-th step, followed by gluing, all expressed via IicProdIoc b (b+1).

Русский

Если a ≤ b, то partialTraj κ a (b+1) равно композиции id на левую часть, затем шаг k и склейка через IicProdIoc b (b+1).

LaTeX

$$$\mathrm{partialTraj}(κ,a,b+1) = (\mathrm{id} \timesₖ (κ b).map(\mathrm{piSingleton} b)) \circ\!_{κ} \mathrm{partialTraj}(κ,a,b) \;\mapsto\; \mathrm{IicProdIoc}(b, b+1)$$$

Lean4

/-- If `b ≤ a`, given the trajectory up to time `a`, the trajectory up to time `b` is
deterministic and is equal to the restriction of the trajectory up to time `a`. -/
theorem partialTraj_le (hba : b ≤ a) :
    partialTraj κ a b = deterministic (frestrictLe₂ hba) (measurable_frestrictLe₂ _) := by rw [partialTraj, dif_pos hba]

Похожие утверждения