MGFDerivative.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GammaFPP.exp_derivative_domination line 15

theorem OAI.GammaFPP.hasDerivAt_integral_exp_zero line 35

Source documentation

A nonnegative measurable function with a positive exponential moment is integrable, and its moment-generating function has derivative equal to its mean at zero. Finiteness of the measure follows by domination.

theorem hasDerivAt_integral_exp_zero {Ω : Type*} [MeasurableSpace Ω]
    {P : Measure Ω} {F : Ω → ℝ} (hF : Measurable F)
    (hpos : ∀ᵐ ω ∂P, 0 ≤ F ω) {c : ℝ} (hc : 0 < c)
    (hexp : Integrable (fun ω => exp (c*F ω)) P) :
    Integrable F P ∧
      HasDerivAt (fun t : ℝ => ∫ ω, exp (t*F ω) ∂P) (∫ ω, F ω ∂P) 0 := by
…

theorem OAI.GammaFPP.hasDerivAt_cgf_zero_of_nonneg_exp line 68

Source documentation

The probability cgf has derivative EF at zero, by the real log chain rule.

theorem hasDerivAt_cgf_zero_of_nonneg_exp {Ω : Type*} [MeasurableSpace Ω]
    {P : Measure Ω} [IsProbabilityMeasure P] {F : Ω → ℝ}
    (hF : Measurable F) (hpos : ∀ᵐ ω ∂P, 0 ≤ F ω) {c : ℝ} (hc : 0 < c)
    (hexp : Integrable (fun ω => exp (c*F ω)) P) :
    HasDerivAt (cgf F P) (∫ ω, F ω ∂P) 0 := by
…