charFun_eq_integral_innerProbChar

English

For each t, the characteristic function equals the integral of the bounded continuous function innerProbChar evaluated at t: χ_μ(t) = ∫ v innerProbChar(t,v) dμ(v).

Русский

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

LaTeX

$$$$\\chi_{\\mu}(t) = \\int_{E} \\mathrm{innerProbChar}(t,v) \\, d\\mu(v).$$$$

Lean4

/-- `charFun` as the integral of a bounded continuous function. -/
theorem charFun_eq_integral_innerProbChar : charFun μ t = ∫ v, innerProbChar t v ∂μ := by
  simp [charFun_apply, innerProbChar_apply]

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