probCharDual_zero — Mathlib

English

A bound continuous probability character for dual spaces is constructed and analyzed via inner products and exponentials.

Русский

Строится ограниченная непрерывная характеристическая функция для двойственных пространств через внутреннее произведение и экспоненту.

LaTeX

$$probCharDual(L) : F →ᵇ ℂ$$

Lean4

@[simp]
theorem probCharDual_zero : probCharDual (0 : StrongDual ℝ F) = 1 := by simp [probCharDual]

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