OAI/Probability/GammaPassage/TiltEnvelope.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.Tilt.gamma_likelihood_envelope line 9

   Source documentation

   A shape-dependent exponential envelope for the Gamma likelihood moment.

   lemma gamma_likelihood_envelope {shape : ℝ} (hs : 0 < shape)
       (δ : ℝ) (hδ : 0 ≤ δ) (hδ' : δ ≤ 1/2) (M : ℕ) :
       (1-δ^2)^(-shape*(M : ℝ)) ≤ exp (2*shape*M*δ^2) := by
   …

2. theorem OAI.GammaFPP.Tilt.finite_edge_tilt_probability_sq_exp_bound line 26