iteratedDeriv_two_cgf_eq_integral

English

For v in the interior, iteratedDeriv_2 cgf at v equals the integral of (X − deriv(cgf)(v))^2 e^{vX} dμ divided by mgf(X, μ)(v).

Русский

Для v вInterior, вторая итерационная производная cgf равна интегралу по μ от (X − deriv(cgf)(v))^2 e^{vX} делённому на mgf(X, μ)(v).

LaTeX

$$$\\mathrm{iteratedDeriv}_2(\\mathrm{cgf}(X,\\mu), v) = \\dfrac{\\int (X(\\omega) - \\mathrm{deriv}(\\mathrm{cgf}(X,\\mu))(v))^2 e^{v X(\\omega)} d\\mu(\\omega)}{\\mathrm{mgf}(X,\\mu)(v)}$ for $v\\in\\mathrm{int}(\\mathrm{integrableExpSet}(X,\\mu)).$$$

Lean4

theorem iteratedDeriv_two_cgf_eq_integral (h : v ∈ interior (integrableExpSet X μ)) :
    iteratedDeriv 2 (cgf X μ) v = μ[fun ω ↦ (X ω - deriv (cgf X μ) v) ^ 2 * exp (v * X ω)] / mgf X μ v :=
  by
  by_cases hμ : μ = 0
  · simp [hμ, iteratedDeriv_succ]
  rw [iteratedDeriv_two_cgf h]
  calc
    (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2
    _ =
        (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ - 2 * (∫ ω, X ω * exp (v * X ω) ∂μ) * deriv (cgf X μ) v +
            deriv (cgf X μ) v ^ 2 * mgf X μ v) /
          mgf X μ v :=
      by
      rw [add_div, sub_div, sub_add]
      congr 1
      rw [mul_div_cancel_right₀, deriv_cgf h]
      · ring
      · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
    _ = (∫ ω, ((X ω) ^ 2 - 2 * X ω * deriv (cgf X μ) v + deriv (cgf X μ) v ^ 2) * exp (v * X ω) ∂μ) / mgf X μ v :=
      by
      congr 1
      simp_rw [add_mul, sub_mul]
      have h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * exp (v * X ω)) μ :=
        by
        simp_rw [mul_assoc, mul_comm (deriv (cgf X μ) v)]
        refine Integrable.const_mul ?_ _
        simp_rw [← mul_assoc]
        refine Integrable.mul_const ?_ _
        convert integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 1
        simp
      rw [integral_add]
      rotate_left
      · exact (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2).sub h_int
      · exact (interior_subset (s := integrableExpSet X μ) h).const_mul _
      rw [integral_sub (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2) h_int]
      congr
      · rw [← integral_const_mul, ← integral_mul_const]
        congr with ω
        ring
      · rw [integral_const_mul, mgf]
    _ = (∫ ω, (X ω - deriv (cgf X μ) v) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v :=
      by
      congr with ω
      ring

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