OAI/Probability/GammaPassage/TiltMoment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.squareTheta line 13
2. lemma OAI.GammaFPP.shrink_likelihood_sq line 16
3. lemma OAI.GammaFPP.square_shifted_rate line 26
4. lemma OAI.GammaFPP.squareTheta_lt_rate line 31
5. lemma OAI.GammaFPP.square_moment_coefficient line 38
6. theorem OAI.GammaFPP.gamma_shrink_likelihood_sq_integrable line 68

   Source documentation

   The square of the shrinking likelihood is integrable under the Gamma law.

   theorem gamma_shrink_likelihood_sq_integrable {shape rate delta : ℝ}
       (hshape : 0 < shape) (hrate : 0 < rate) (hlo : -1 < delta) (hhi : delta < 1) :
       Integrable (fun x : ℝ => gammaShrinkLikelihood shape rate delta x ^ 2)
         (gammaMeasure shape rate) := by
   …

   Mentions: OAI.GammaFPP.gammaShrinkLikelihood

7. theorem OAI.GammaFPP.gamma_shrink_likelihood_second_moment line 79

   Source documentation

   The second moment of the likelihood for one coordinate.

   theorem gamma_shrink_likelihood_second_moment {shape rate delta : ℝ}
       (hshape : 0 < shape) (hrate : 0 < rate) (hlo : -1 < delta) (hhi : delta < 1) :
       (∫ x : ℝ, gammaShrinkLikelihood shape rate delta x ^ 2 ∂gammaMeasure shape rate) =
         (1 - delta ^ 2) ^ (-shape) := by
   …

   Mentions: OAI.GammaFPP.gammaShrinkLikelihood

8. theorem OAI.GammaFPP.gamma_shrink_likelihood_second_lintegral line 97

   Source documentation

   The nonnegative second moment used in finite-product likelihood arguments.

   theorem gamma_shrink_likelihood_second_lintegral {shape rate delta : ℝ}
       (hshape : 0 < shape) (hrate : 0 < rate) (hlo : -1 < delta) (hhi : delta < 1) :
       (∫⁻ x : ℝ, (ENNReal.ofReal (gammaShrinkLikelihood shape rate delta x)) ^ 2
           ∂gammaMeasure shape rate) = ENNReal.ofReal ((1 - delta ^ 2) ^ (-shape)) := by
   …

   Mentions: OAI.GammaFPP.gammaShrinkLikelihood