English
For μ on ℝ, complexMGF id μ at t·I equals the real characteristic function χ_μ(t).
Русский
Для меры μ на ℝ комплексная MGF для функцииId при t·I равна χ_μ(t).
LaTeX
$$$ complexMGF\ id\ μ (t \cdot I) = charFun\ μ\ t $$$
Lean4
/-- For `z : ℂ` with `z.re ∈ interior (integrableExpSet X μ)`, the derivative of the function
`z' ↦ μ[X ^ n * cexp (z' * X)]` at `z` is `μ[X ^ (n + 1) * cexp (z * X)]`. -/
theorem hasDerivAt_integral_pow_mul_exp (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) :
HasDerivAt (fun z ↦ μ[fun ω ↦ X ω ^ n * cexp (z * X ω)]) μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] z :=
by
have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet hz
have hz' := hz
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hz'
obtain ⟨l, u, hlu, h_subset⟩ := hz'
let t := ((z.re - l) ⊓ (u - z.re)) / 2
have h_pos : 0 < (z.re - l) ⊓ (u - z.re) := by simp [hlu.1, hlu.2]
have ht : 0 < t := half_pos h_pos
refine
(hasDerivAt_integral_of_dominated_loc_of_deriv_le (bound := fun ω ↦
|X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) (F := fun z ω ↦ X ω ^ n * cexp (z * X ω)) (F' := fun z ω ↦
X ω ^ (n + 1) * cexp (z * X ω)) (half_pos ht) ?_ ?_ ?_ ?_ ?_ ?_).2
· exact .of_forall fun z ↦ by fun_prop
· exact integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet hz n
· fun_prop
· refine ae_of_all _ fun ω ε hε ↦ ?_
simp only [norm_mul, norm_pow, norm_real, Real.norm_eq_abs]
rw [Complex.norm_exp]
simp only [mul_re, ofReal_re, ofReal_im, mul_zero, sub_zero]
gcongr
have : ε = z + (ε - z) := by simp
rw [this, add_re, add_mul]
gcongr _ + ?_
refine (le_abs_self _).trans ?_
rw [abs_mul]
gcongr
refine (abs_re_le_norm _).trans ?_
simp only [Metric.mem_ball, dist_eq_norm] at hε
exact hε.le
· refine integrable_pow_abs_mul_exp_add_of_integrable_exp_mul ?_ ?_ ?_ ?_ (t := t) (n + 1)
· exact h_subset (add_half_inf_sub_mem_Ioo hlu)
· exact h_subset (sub_half_inf_sub_mem_Ioo hlu)
· positivity
· exact lt_of_lt_of_le (by simp [ht]) (le_abs_self _)
· refine ae_of_all _ fun ω ε hε ↦ ?_
simp only
simp_rw [pow_succ, mul_assoc]
refine HasDerivAt.const_mul _ ?_
simp_rw [← smul_eq_mul, Complex.exp_eq_exp_ℂ]
convert hasDerivAt_exp_smul_const (X ω : ℂ) ε using 1
rw [smul_eq_mul, mul_comm]
