MGF.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GammaFPP.gamma_weighted_density line 17

Source documentation

Exponential weighting changes the Gamma rate from rate to rate - theta.

lemma gamma_weighted_density {shape rate theta : ℝ}
    (hshape : 0 < shape) (hrate : 0 < rate) (htheta : theta < rate) (x : ℝ) :
    gammaPDF shape rate x * ENNReal.ofReal (exp (theta * x)) =
      ENNReal.ofReal ((rate / (rate - theta)) ^ shape) *
        gammaPDF shape (rate - theta) x := by
…

theorem OAI.GammaFPP.gamma_lintegral_exp line 53

Source documentation

The nonnegative exponential moment from the normalized density with shifted rate.

theorem gamma_lintegral_exp {shape rate theta : ℝ}
    (hshape : 0 < shape) (hrate : 0 < rate) (htheta : theta < rate) :
    (∫⁻ x : ℝ, ENNReal.ofReal (exp (theta * x)) ∂gammaMeasure shape rate) =
      ENNReal.ofReal ((rate / (rate - theta)) ^ shape) := by
…

theorem OAI.GammaFPP.gamma_integrable_exp line 66

Source documentation

Exponential functions are integrable under the Gamma law for theta < rate.

theorem gamma_integrable_exp {shape rate theta : ℝ}
    (hshape : 0 < shape) (hrate : 0 < rate) (htheta : theta < rate) :
    Integrable (fun x : ℝ => exp (theta * x)) (gammaMeasure shape rate) := by
…

theorem OAI.GammaFPP.gamma_integral_exp line 75

Source documentation

Gamma exponential moments, as in paper 210, Lemma df:ga:moment.

theorem gamma_integral_exp {shape rate theta : ℝ}
    (hshape : 0 < shape) (hrate : 0 < rate) (htheta : theta < rate) :
    (∫ x : ℝ, exp (theta * x) ∂gammaMeasure shape rate) =
      (rate / (rate - theta)) ^ shape := by
…