English
For a > 0 and r > 0, cdf(gammaMeasure(a, r))(x) equals the integral of gammaPDFReal over (−∞, x].
Русский
Для a > 0 и r > 0 cdf(gammaMeasure(a, r))(x) равен интегралу gammaPDFReal(a, r) по (−∞, x].
LaTeX
$$$cdf(\gammaMeasure(a,r))(x) = \int_{(-\infty, x]} \gammaPDFReal(a,r)(t) dt$$$
Lean4
/-- The characteristic function of a Gaussian measure `μ` has value
`exp (μ[L] * I - Var[L; μ] / 2)` at `L : Dual ℝ E`. -/
theorem charFunDual_eq (L : StrongDual ℝ E) : charFunDual μ L = exp (μ[L] * I - Var[L; μ] / 2) := by
calc
charFunDual μ L
_ = charFun (μ.map L) 1 := by rw [charFunDual_eq_charFun_map_one]
_ = charFun (gaussianReal (μ[L]) (Var[L; μ]).toNNReal) 1 := by rw [IsGaussian.map_eq_gaussianReal L]
_ = exp (μ[L] * I - Var[L; μ] / 2) := by
rw [charFun_gaussianReal]
simp only [ofReal_one, one_mul, Real.coe_toNNReal', one_pow, mul_one]
congr
· rw [integral_complex_ofReal]
· simp only [sup_eq_left]
exact variance_nonneg _ _
