← Mathematical handbook

theorem Verification.tendsto_lower_tail_average (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {f : ℝ → ℝ} {L : ℝ} (hi : MeasureTheory.Integrable f μ) (hp : ∀ (a : ℝ), 0 < μ.real (Set.Iic a)) (ht : Filter.Tendsto f Filter.atBot (nhds L)) : Filter.Tendsto (fun (a : ℝ) => (∫ (x : ℝ) in Set.Iic a, f x ∂μ) / μ.real (Set.Iic a)) Filter.atBot (nhds L)