partialTraj_zero — Mathlib

English

If each κ(n) is finite in the sense of IsFiniteKernel, then for any a,b the kernel partialTraj κ a b is also IsSFiniteKernel.

Русский

Если для всех n ядро κ(n) эфективно конечное, то partialTraj κ a b тоже конечное в смысле IsSFiniteKernel.

LaTeX

$$$\forall a,b:\, \mathrm{IsSFiniteKernel}(\mathrm{partialTraj}(κ,a,b))$ under the hypothesis $\forall n, \mathrm{IsFiniteKernel}(κ(n))$$$

Lean4

@[simp]
theorem partialTraj_zero : partialTraj κ a 0 = deterministic (frestrictLe₂ (zero_le a)) (measurable_frestrictLe₂ _) :=
  by rw [partialTraj_le (zero_le a)]

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