lintegral_traj — Mathlib

English

If f is measurable, the lintegral of f over traj κ a x0 equals the lintegral of f after updating with updateFinset on Iic a.

Русский

Пусть f измеримо; линеграль по траектории до времени a равен линегралу после обновления траекторий.

LaTeX

$$$\\int^{-} f \\, d\\operatorname{traj}_κ a x_0 = \\int^{-} f(\\operatorname{updateFinset} x (\\mathsf{Iic}\\,a) x_0) \\, d\\operatorname{traj}_κ a x_0$$$

Lean4

theorem lintegral_traj {a : ℕ} (x₀ : Π i : Iic a, X i) {f : (Π n, X n) → ℝ≥0∞} (mf : Measurable f) :
    ∫⁻ x, f x ∂traj κ a x₀ = ∫⁻ x, f (updateFinset x (Iic a) x₀) ∂traj κ a x₀ :=
  lintegral_traj₀ x₀ mf.aemeasurable

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