← Mathematical handbook

theorem Verification.concentration_integral_bound (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (f : ℝ → ℝ) (hf : Measurable f) {B η δ : ℝ} (hB : ∀ (x : ℝ), |f x| ≤ B) (hη : 0 ≤ η) (hloc : ∀ (x : ℝ), |x - 1| < δ → |f x - f 1| ≤ η) : |∫ (x : ℝ), f x ∂μ - f 1| ≤ η + 2 * B * μ.real {x : ℝ | δ ≤ |x - 1|}

theorem Verification.tendsto_integral_of_concentration {ι : Type u_1} {l : Filter ι} (μ : ι → MeasureTheory.ProbabilityMeasure ℝ) (hμ : ∀ δ > 0, Filter.Tendsto (fun (i : ι) => (↑(μ i)).real {x : ℝ | δ ≤ |x - 1|}) l (nhds 0)) (f : ℝ → ℝ) (hf : Measurable f) (hc : ContinuousAt f 1) {B : ℝ} (hB : ∀ (x : ℝ), |f x| ≤ B) : Filter.Tendsto (fun (i : ι) => ∫ (x : ℝ), f x ∂↑(μ i)) l (nhds (f 1))

theorem Verification.gammaPrecision_integral_tendsto {ι : Type u_1} {l : Filter ι} (a : ι → ℝ) (ha : ∀ (i : ι), 0 < a i) (ht : Filter.Tendsto a l Filter.atTop) (f : ℝ → ℝ) (hf : Measurable f) (hc : ContinuousAt f 1) {B : ℝ} (hB : ∀ (x : ℝ), |f x| ≤ B) : Filter.Tendsto (fun (i : ι) => ∫ (x : ℝ), f x ∂ProbabilityTheory.gammaMeasure (a i) (a i)) l (nhds (f 1))