English
If z lies in the interior of the integrable-exponential set, complexMGF X μ is differentiable at z with derivative μ[X ω · exp(z X ω)].
Русский
Если z лежит во внутренности множества интегрируемого экспоненциала, комплексная MGf X μ дифференцируема в z, ее производная равна μ[X ω · exp(z X ω)].
LaTeX
$$$ \text{HasDerivAt}(\text{complexMGF } X μ, \int X(ω) e^{z X(ω)} dμ(ω), z) \quad \text{для } z \text{ с } z.re \in \operatorname{int}(\text{integrableExpSet}(X, μ)). $$$
Lean4
/-- **Lévy's generalization of the Borel-Cantelli lemma**: given a sequence of sets `s` and a
filtration `ℱ` such that for all `n`, `s n` is `ℱ n`-measurable, `limsup s atTop` is almost
everywhere equal to the set for which `∑ k, ℙ(s (k + 1) | ℱ k) = ∞`. -/
theorem ae_mem_limsup_atTop_iff (μ : Measure Ω) [IsFiniteMeasure μ] {s : ℕ → Set Ω}
(hs : ∀ n, MeasurableSet[ℱ n] (s n)) :
∀ᵐ ω ∂μ,
ω ∈ limsup s atTop ↔
Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|ℱ k]) ω) atTop atTop :=
by
rw [← limsup_nat_add s 1, Set.limsup_eq_tendsto_sum_indicator_atTop (zero_lt_one (α := ℝ)) (fun n ↦ s (n + 1))]
exact tendsto_sum_indicator_atTop_iff' hs
