← Mathematical handbook

theorem Verification.gammaPrecision_concentration_bound {a ε : ℝ} (ha : 0 < a) (hε : 0 < ε) : (ProbabilityTheory.gammaMeasure a a).real {t : ℝ | ε ≤ |t - 1|} ≤ a⁻¹ / ε ^ 2

theorem Verification.gammaPrecision_concentrates {ι : Type u_1} {l : Filter ι} (a : ι → ℝ) (ha : ∀ (i : ι), 0 < a i) (ht : Filter.Tendsto a l Filter.atTop) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (i : ι) => (ProbabilityTheory.gammaMeasure (a i) (a i)).real {t : ℝ | ε ≤ |t - 1|}) l (nhds 0)