charFun_apply_real

Mathlib.MeasureTheory.Measure.CharacteristicFunction

URI: https://scilib.ai/kg/mathlib#MeasureTheory.charFun_apply_real

English

If μ is a measure on the real line and t ∈ ℝ, then the characteristic function is χ_μ(t) = ∫_ℝ e^{i t x} dμ(x).

Русский

Пусть μ — мера на ℝ, и t ∈ ℝ. Тогда χ_μ(t) = ∫_ℝ e^{i t x} dμ(x).

LaTeX

$$$$\\chi_{\\mu}(t) = \\int_{\\mathbb{R}} e^{i t x} \\, d\\mu(x).$$$$

Lean4

theorem charFun_apply_real {μ : Measure ℝ} (t : ℝ) : charFun μ t = ∫ x, exp (t * x * I) ∂μ := by simp [charFun_apply]

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

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

Разделы

Аффилиация

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