OAI/Probability/GammaPassage/TiltComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.withDensity_sq_le_second_moment line 11

   Source documentation

   Cauchy–Schwarz for an extended nonnegative density and a measurable event.

   theorem withDensity_sq_le_second_moment {Ω : Type*} [MeasurableSpace Ω]
       (P : Measure Ω) (L : Ω → ℝ≥0∞) (hL : Measurable L)
       (A : Set Ω) (hA : MeasurableSet A) :
       ((P.withDensity L) A)^2 ≤ (∫⁻ x, (L x)^2 ∂P)*P A := by
   …

2. theorem OAI.GammaFPP.finite_gamma_scaled_probability_sq_bound line 31

   Source documentation

   A second-moment bound for scaled finite Gamma event probabilities when -1 < delta < 1.

   theorem finite_gamma_scaled_probability_sq_bound
       {ι : Type*} [Fintype ι] {shape rate delta : ℝ}
       (hs : 0 < shape) (hr : 0 < rate) (hlo : -1 < delta) (hhi : delta < 1)
       (A : Set (ι → ℝ)) (hA : MeasurableSet A) :
       ((finiteGammaMeasure (ι := ι) shape rate).map
   …

   Mentions: OAI.GammaFPP.finiteGammaMeasure