partialTraj_self

Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.partialTraj_self

English

For any a, the trajectory truncated at the same time equals the identity kernel: partialTraj κ a a = id.

Русский

Для любого a траектория, усечённая на время a, совпадает с тождественным ядром: partialTraj κ a a = id.

LaTeX

$$$\mathrm{partialTraj}(κ,a,a) = \mathrm{Kernel.id}$$$

Lean4

@[simp]
theorem partialTraj_self (a : ℕ) : partialTraj κ a a = Kernel.id := by rw [partialTraj_le le_rfl]; rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru