charFun_eq_integral_probChar

Mathlib.MeasureTheory.Measure.CharacteristicFunction

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

English

For every t, χ_μ(t) equals the integral of probChar applied to ⟪x,t⟫: χ_μ(t) = ∫_E (probChar(⟪x,t⟫) ) dμ(x).

Русский

Для каждого t верно χ_μ(t) = ∫_E probChar(⟪x,t⟫) dμ(x).

LaTeX

$$$$\\chi_{\\mu}(t) = \\int_E (\\mathrm{probChar}(\\langle x,t\\rangle)) \\, d\\mu(x).$$$$

Lean4

theorem charFun_eq_integral_probChar (t : E) : charFun μ t = ∫ x, (probChar ⟪x, t⟫ : ℂ) ∂μ := by
  simp [charFun_apply, probChar_apply]

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

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

Разделы

Аффилиация

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