theorem IntegralCriterion.cauchy_of_tendsto {F : ℝ → ℝ} {L : ℝ} (hF : Filter.Tendsto F Filter.atTop (nhds L)) (c : ℝ) : c > 0 → ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (y : ℝ), x ≤ y → |F y - F x| < c

theorem IntegralCriterion.integrableOn_g_Ioc (f : ℝ → ℝ) (hf : Monotone f) (a b : ℝ) (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (f t - t) / t ^ 2) (Set.Ioc a b) MeasureTheory.volume

theorem IntegralCriterion.integral_Ioc_split' {g : ℝ → ℝ} {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) (hg1 : MeasureTheory.IntegrableOn g (Set.Ioc a b) MeasureTheory.volume) (hg2 : MeasureTheory.IntegrableOn g (Set.Ioc b c) MeasureTheory.volume) : ∫ (x : ℝ) in Set.Ioc a c, g x = (∫ (x : ℝ) in Set.Ioc a b, g x) + ∫ (x : ℝ) in Set.Ioc b c, g x

theorem IntegralCriterion.integral_const_Ioc {a b : ℝ} (hab : a ≤ b) (c : ℝ) : ∫ (x : ℝ) in Set.Ioc a b, c = c * (b - a)

theorem IntegralCriterion.upper_bound_of_convergent_integral (f : ℝ → ℝ) (hf_mono : Monotone f) {L : ℝ} (hL : Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioc 1 x, (f t - t) / t ^ 2) Filter.atTop (nhds L)) {lam : ℝ} (hlam : 1 < lam) : ∀ᶠ (x : ℝ) in Filter.atTop, f x < lam * x

theorem IntegralCriterion.lower_bound_of_convergent_integral (f : ℝ → ℝ) (hf_mono : Monotone f) {L : ℝ} (hL : Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioc 1 x, (f t - t) / t ^ 2) Filter.atTop (nhds L)) {lam : ℝ} (hlam : 1 < lam) : ∀ᶠ (x : ℝ) in Filter.atTop, x / lam < f x

theorem IntegralCriterion.lem_16_8_integral_criterion (f : ℝ → ℝ) (hf_mono : Monotone f) (hf_conv : ∃ (L : ℝ), Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioc 1 x, (f t - t) / t ^ 2) Filter.atTop (nhds L)) : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => f x) fun (x : ℝ) => x

theorem lem_16_8 (f : ℝ → ℝ) (hf_mono : Monotone f) (hf_conv : ∃ (L : ℝ), Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioc 1 x, (f t - t) / t ^ 2) Filter.atTop (nhds L)) : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => f x) fun (x : ℝ) => x

@[reducible, inline]

abbrev Lem168.lem_16_8_integral_criterion (f : ℝ → ℝ) (hf_mono : Monotone f) (hf_conv : ∃ (L : ℝ), Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioc 1 x, (f t - t) / t ^ 2) Filter.atTop (nhds L)) : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => f x) fun (x : ℝ) => x