English
For a > 0 and r > 0, cdf(gammaMeasure(a, r))(x) equals toReal of the lintegral of gammaPDF over (−∞, x].
Русский
Для a > 0 и r > 0 CDF гамма-меры равен toReal(lintegral гамма-плотности по (−∞, x]).
LaTeX
$$$cdf(\gammaMeasure(a,r))(x) = \operatorname{toReal}\left(\int^{-}_{t\in Iic(x)} \gammaPDF(a,r)(t) \right)$$$
Lean4
/-- A finite measure is Gaussian iff its characteristic function has value
`exp (μ[L] * I - Var[L; μ] / 2)` for every `L : Dual ℝ E`. -/
theorem isGaussian_iff_charFunDual_eq {μ : Measure E} [IsFiniteMeasure μ] :
IsGaussian μ ↔ ∀ L : StrongDual ℝ E, charFunDual μ L = exp (μ[L] * I - Var[L; μ] / 2) :=
by
refine ⟨fun h ↦ h.charFunDual_eq, fun h ↦ ⟨fun L ↦ Measure.ext_of_charFun ?_⟩⟩
ext u
rw [charFun_map_eq_charFunDual_smul L u, h (u • L), charFun_gaussianReal]
simp only [ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul, ofReal_mul, Real.coe_toNNReal']
congr
· rw [integral_const_mul, integral_complex_ofReal]
· rw [max_eq_left (variance_nonneg _ _), mul_comm, ← ofReal_pow, ← ofReal_mul, ← variance_mul]
congr
