Asymptotics conversions from equivalents

Stream: Is there code for X?

[Ryan Lahfa]

I'm looking at the asymptotics API to prove that $log(1+x)/x \to 0$ when $x \to +\infty$, and it seems like there is no theorem to convert an equivalent to an is_o relation.

What I'm looking for is, if $u \sim v$, proving $v = o(g)$ is equivalent to proving $u = o(g)$.
Is there a nice way to do it or should there be a convert theorem (that I might have missed)?

Here's a MWE to illustrate what I'm trying to do:

import analysis.special_functions.exp_log
import analysis.asymptotics.asymptotic_equivalent
import analysis.asymptotics.asymptotics

open filter
open_locale asymptotics topological_space

lemma asymptotics.is_equivalent.left_comp_log {f g: ℝ → ℝ} {l: filter ℝ}
  (h: f ~[l] g) (htop: tendsto f l at_top): real.log ∘ f ~[l] real.log ∘ g := sorry

lemma tendsto_log1_plus_x_under_x_at_top_nhds_1:
  tendsto (λ (x: ℝ), real.log (1 + x) / x) at_top (𝓝 0) :=
begin
  have h: tendsto (λ (x : ℝ), 1 + x) at_top at_top,
  from tendsto_at_top_mono (by simp [zero_le_one]) (tendsto_id),
  suffices : asymptotics.is_o real.log id at_top,
  {
    apply asymptotics.is_o.tendsto_0,
    -- here I would like to prove log(x) = o(x) is enough to prove log(1 + x) = o(x) knowing log(1 + x) ~ log(x) by left_comp_log.
    sorry,
  },

  have : asymptotics.is_o id real.exp at_top := sorry,
  convert asymptotics.is_o.comp_tendsto this real.tendsto_log_at_top using 1,
  ext, simp,
  sorry,
end

[Anatole Dedecker]

I'm afraid this lemma doesn't exist, but it definitely should. I can't do Lean right now, but I think you should be able to get it by saying that u - v = o(v) = o(g) since v = o(g) (docs#asymptotics.is_o.trans), which then implies u = u - v + v = o(g) (docs#asymptotics.is_o.add)

[Ryan Lahfa]

Anatole Dedecker said:

I'm afraid this lemma doesn't exist, but it definitely should. I can't do Lean right now, but I think you should be able to get it by saying that u - v = o(v) = o(g) since v = o(g) (docs#asymptotics.is_o.trans), which then implies u = u - v + v = o(g) (docs#asymptotics.is_o.add)

Thanks!

[Ryan Lahfa]

FWIW, here's the proof:

lemma asymptotics.is_equivalent_is_o_of_equivalent_of_o {u v w: ℝ → ℝ} {l: filter ℝ}
  (h_equiv: u ~[l] v) (ho: is_o v w l): is_o u w l :=
  begin
    convert is_o.add (is_o.trans h_equiv ho) ho,
    simp,
  end

[Ryan Lahfa]

Enjoy the final proof:

import analysis.special_functions.exp_log
import analysis.asymptotics.asymptotic_equivalent
import analysis.asymptotics.asymptotics
import analysis.asymptotics.specific_asymptotics

open filter asymptotics
open_locale asymptotics topological_space

lemma eventually_nonzero_of_tendsto_at_top {f: ℝ → ℝ} {l: filter ℝ}
  (htop: tendsto f l at_top): ∀ᶠ x in l, f x ≠ 0 :=
  begin
    have: ∀ᶠ (y: ℝ) in at_top, y ≠ 0,
    {
      simp [eventually_at_top],
      exact ⟨ 1, λ b hb, by linarith only [hb] ⟩,
    },
    convert tendsto.eventually htop this,
  end

lemma eventually_false_of_not {α} {p q: α → Prop} {l: filter α}
  (hnp: ∀ᶠ x in l, ¬ p x): (∀ᶠ x in l, p x → q x) :=
  eventually.mono hnp (λ x hnpx hpx, absurd hpx hnpx)

lemma asymptotics.is_o.of_tendsto_at_top {f: ℝ → ℝ} {l: filter ℝ}
  (htop: tendsto f l at_top): is_o (1: ℝ → ℝ) f l :=
  begin
    refine (asymptotics.is_o_iff_tendsto' _).2 _,
    exact eventually_false_of_not (eventually_nonzero_of_tendsto_at_top htop),
    convert tendsto.inv_tendsto_at_top htop,
    ext, simp,
  end

lemma asymptotics.is_equivalent.left_comp_log {f g: ℝ → ℝ} {l: filter ℝ}
  (h: f ~[l] g) (htop: tendsto f l at_top): real.log ∘ f ~[l] real.log ∘ g :=
  begin
    have fact1 : is_o (real.log ∘ f - real.log ∘ g) (1: ℝ → ℝ) l,
    {
      have hnonvanish: ∀ᶠ x in l, g x ≠ 0 := (eventually_nonzero_of_tendsto_at_top (is_equivalent.tendsto_at_top h htop)),
      refine (asymptotics.is_o_iff_tendsto _).2 _,
      simp only [forall_false_left, forall_const, pi.one_apply, one_ne_zero],
      simp only [function.comp_app, pi.one_apply, div_one, pi.sub_apply],
      refine tendsto.congr'
        (_: real.log ∘ (f / g) =ᶠ[l] (λ (x: ℝ), real.log (f x) - real.log (g x))) _,
      convert eventually.mono _ (λ (x: ℝ) (hx: f x ≠ 0 ∧ g x ≠ 0), @real.log_div (f x) (g x) hx.1 hx.2),
      exact (eventually_nonzero_of_tendsto_at_top htop).and hnonvanish,
      convert (real.continuous_at_log _).tendsto.comp
        ((is_equivalent_iff_tendsto_one hnonvanish).1 h),
      all_goals { simp, },
    },
    have fact2 : is_o 1 (real.log ∘ g) l :=
      asymptotics.is_o.of_tendsto_at_top
        (real.tendsto_log_at_top.comp
        ((asymptotics.is_equivalent.tendsto_at_top_iff h).1 htop)),
    exact is_o.trans fact1 fact2,
  end

lemma asymptotics.is_equivalent.left_comp_log' {f g: ℝ → ℝ} {l: filter ℝ}
  (h: f ~[l] g) (htop: tendsto g l at_top): real.log ∘ f ~[l] real.log ∘ g :=
  asymptotics.is_equivalent.left_comp_log h ((asymptotics.is_equivalent.tendsto_at_top_iff h).2 htop)

lemma asymptotics.is_equivalent.is_o_of_equivalent_of_o {u v w: ℝ → ℝ} {l: filter ℝ}
  (h_equiv: u ~[l] v) (ho: is_o v w l): is_o u w l :=
  begin
    convert is_o.add (is_o.trans h_equiv ho) ho,
    simp,
  end

lemma log_is_o_of_id:
  is_o real.log id at_top :=
  begin
    refine asymptotics.is_o.congr'
    (_: id ∘ real.log =ᶠ[at_top] real.log)
    (_: real.exp ∘ real.log =ᶠ[at_top] id) _,
    simp,
    {
      refine eventually.mono _ (λ (x: ℝ) (hx: 0 < x), real.exp_log hx),
      rw [eventually_at_top],
      exact ⟨ 1, λ a ha, by linarith [ha] ⟩,
    },
    {
      refine asymptotics.is_o.comp_tendsto
      _ real.tendsto_log_at_top,
      refine
        (asymptotics.is_o_iff_tendsto'
          (eventually_false_of_not (eventually_of_forall real.exp_ne_zero))).2
        _,
      convert real.tendsto_pow_mul_exp_neg_at_top_nhds_0 1,
      field_simp [real.exp_neg],
    }
  end

lemma tendsto_log1_plus_x_under_x_at_top_nhds_1:
  tendsto (λ (x: ℝ), real.log (1 + x) / x) at_top (𝓝 0) :=
begin
  suffices : asymptotics.is_o real.log id at_top,
  {
    apply asymptotics.is_o.tendsto_0,
    refine
      asymptotics.is_equivalent.is_o_of_equivalent_of_o
      (_: (λ (x: ℝ), real.log (1 + x)) ~[at_top] real.log) this,
    convert
      asymptotics.is_equivalent.left_comp_log'
      (_: (λ (x: ℝ), 1 + x) ~[at_top] id) tendsto_id,
    convert (asymptotics.is_equivalent.refl).add_is_o _,
    convert asymptotics.is_o_pow_pow_at_top_of_lt zero_lt_one,
    simp,
    exactI real.order_topology, -- why is this needed?
  },
  exact log_is_o_of_id,
end

I find it strange that I need to do exactI real.order_topology but I'm super happy with the result :-) (the original proof involved to prove L'Hopital Rule + derivatives stuff for logs for +∞/+∞ and it was getting too messy.)

[Patrick Massot]

The I in exactI can't be needed. It means "please put something in the type class game for later use" while there is no later tactic there.

[Patrick Massot]

Presumably one of the tactic does instance search too late (apply is very prone to do that, and I guess convert can do it too) and you could simply use apply_instance instead of exactI.

[Ryan Lahfa]

Makes sense, then, thanks!

[Anatole Dedecker]

I think at some point I had an epsilon-delta proof of L'Hôpital's rule +∞/+∞ but it was extremely long and boring so I just didn't have the energy to turn it into a PR

[Patrick Massot]

I'm sure you can improve Ryan's proof, filling in missing mathlib lemmas along the way.

[Mario Carneiro]

Patrick Massot said:

The I in exactI can't be needed. It means "please put something in the type class game for later use" while there is no later tactic there.

Actually that's the case with intro-like tactics, but for exact-like tactics the typeclass context is adjusted before the call to exact. exactI e means "use all instances in the local context to elaborate e and use it to finish the goal"

[Patrick Massot]

Yes, I thought about this during dinner.

[Anatole Dedecker]

This took way longer than expected because I wanted to make everything PR-ready (and also because I'm starting to be really tired), but here it is :

import analysis.special_functions.exp_log
import analysis.asymptotics.asymptotic_equivalent
import analysis.asymptotics.asymptotics
import analysis.asymptotics.specific_asymptotics

open filter asymptotics
open_locale asymptotics topological_space

--to mathlib
lemma eventually_ne_at_top {α : Type*} [preorder α] [no_top_order α] (a : α) :
  ∀ᶠ x in at_top, x ≠ a :=
(eventually_gt_at_top a).mono (λ x hx, hx.ne.symm)

--to mathlib (maybe rename is_o_one_iff ?)
lemma asymptotics.is_o_one_iff_left {α 𝕂 E : Type*} [normed_field 𝕂] [normed_group E] {f : α → E}
  {l : filter α} : is_o (1 : α → 𝕂) f l ↔ tendsto (λ x, ∥f x∥) l at_top :=
begin
  change is_o (λ _, 1 : α → 𝕂) f l ↔ _,
  refine ⟨λ h, _, λ h, _⟩,
  { rw (at_top_basis' (1 : ℝ)).tendsto_right_iff,
    intros c hc,
    have : 0 < c := zero_lt_one.trans_le hc,
    convert h.def (inv_pos.mpr this),
    ext x,
    rw [set.mem_Ici, norm_one, ← inv_mul_cancel (this.ne.symm),
        mul_le_mul_left (inv_pos.mpr this)] },
  { rw is_o_iff,
    intros c hc,
    filter_upwards [h.eventually (eventually_ge_at_top c⁻¹)],
    intros x hx,
    rwa [norm_one, ← mul_inv_cancel (hc.ne.symm), mul_le_mul_left hc] }
end

-- to mathlib
lemma asymptotics.is_O_with.eventually_eq_zero_imp {α 𝕂 : Type*} [normed_field 𝕂] {c : ℝ}
  {l : filter α} {f g : α → 𝕂} (h : is_O_with c f g l) : ∀ᶠ x in l, g x = 0 → f x = 0 :=
h.bound.mono (λ x hx hg, by simpa [hg] using hx)

-- to mathlib
lemma asymptotics.is_O.eventually_eq_zero_imp {α 𝕂 : Type*} [normed_field 𝕂]
  {l : filter α} {f g : α → 𝕂} (h : is_O f g l) : ∀ᶠ x in l, g x = 0 → f x = 0 :=
let ⟨c, hc⟩ := h.is_O_with in hc.eventually_eq_zero_imp

-- to mathlib
-- TODO : `tendsto f l at_top` is too strong, `∀ᶠ x in l, ∥f x - 1∥ ≥ ε` should be enough
lemma asymptotics.is_equivalent.left_comp_log_of_tendsto_at_top' {α : Type*} {f g : α → ℝ} {l : filter α}
  (h : f ~[l] g) (htop : tendsto g l at_top) : real.log ∘ f ~[l] real.log ∘ g :=
begin
  have hg : ∀ᶠ x in l, g x ≠ 0 := htop.eventually (eventually_ne_at_top 0),
  have hf : ∀ᶠ x in l, f x ≠ 0 := hg.mp (h.symm.is_O.eventually_eq_zero_imp.mono (λ x, mt)),
  have fact1 : is_o (real.log ∘ f - real.log ∘ g) (1 : α → ℝ) l,
  { refine (asymptotics.is_o_iff_tendsto (λ x (h : (1 : ℝ) = 0), (one_ne_zero h).elim)).2 _,
    simp only [function.comp_app, pi.one_apply, div_one, pi.sub_apply],
    have : tendsto (λ x, real.log (f x / g x)) l (𝓝 0) :=
      real.log_one ▸ ((is_equivalent_iff_tendsto_one hg).mp h).log one_ne_zero,
    refine this.congr' _,
    filter_upwards [hf, hg] (λ x hfx hgx, real.log_div hfx hgx) },
  have fact2 : is_o (1 : α → ℝ) (real.log ∘ g) l :=
    asymptotics.is_o_one_iff_left.mpr (tendsto_norm_at_top_at_top.comp $
      real.tendsto_log_at_top.comp htop),
  exact is_o.trans fact1 fact2
end

-- to mathlib
lemma asymptotics.is_equivalent.left_comp_log_of_tendsto_at_top {α : Type*} {f g : α → ℝ}
  {l : filter α} (h : f ~[l] g) (htop : tendsto f l at_top) :
  real.log ∘ f ~[l] real.log ∘ g :=
asymptotics.is_equivalent.left_comp_log_of_tendsto_at_top' h (h.tendsto_at_top_iff.mp htop)

-- to mathlib
lemma asymptotics.is_o.congr_is_equivalent_left {α E : Type*} [normed_group E] {u v w : α → E}
  {l: filter α} (ho: is_o v w l) (h_equiv: u ~[l] v) : is_o u w l :=
begin
  convert is_o.add (is_o.trans h_equiv ho) ho,
  simp,
end

-- to mathlib
lemma real.is_o_id_exp_at_top : is_o id real.exp at_top :=
begin
  refine (asymptotics.is_o_iff_tendsto $ λ (x : ℝ) hx, (x.exp_pos.ne hx.symm).elim).mpr _,
  convert real.tendsto_div_pow_mul_exp_add_at_top 1 0 1 zero_ne_one (le_refl _),
  ext,
  simp
end

-- to mathlib
lemma real.is_o_log_id_at_top:
  is_o real.log id at_top :=
asymptotics.is_o.congr' (eventually_eq.refl _ _)
  ((eventually_gt_at_top 0).mono $ λ x hx, real.exp_log hx)
  (real.is_o_id_exp_at_top.comp_tendsto real.tendsto_log_at_top)

lemma tendsto_log1_plus_x_under_x_at_top_nhds_0 :
  tendsto (λ (x : ℝ), real.log (1 + x) / x) at_top (𝓝 0) :=
have this : 1 + id ~[at_top] id := (is_equivalent.refl).add_is_o
  (asymptotics.is_o_one_iff_left.mpr tendsto_norm_at_top_at_top),
(real.is_o_log_id_at_top.congr_is_equivalent_left $
  this.left_comp_log_of_tendsto_at_top' tendsto_id).tendsto_0

[Ryan Lahfa]

Anatole Dedecker said:

This took way longer than expected because I wanted to make everything PR-ready (and also because I'm starting to be really tired), but here it is :

import analysis.special_functions.exp_log
import analysis.asymptotics.asymptotic_equivalent
import analysis.asymptotics.asymptotics
import analysis.asymptotics.specific_asymptotics

open filter asymptotics
open_locale asymptotics topological_space

--to mathlib
lemma eventually_ne_at_top {α : Type*} [preorder α] [no_top_order α] (a : α) :
  ∀ᶠ x in at_top, x ≠ a :=
(eventually_gt_at_top a).mono (λ x hx, hx.ne.symm)

--to mathlib (maybe rename is_o_one_iff ?)
lemma asymptotics.is_o_one_iff_left {α 𝕂 E : Type*} [normed_field 𝕂] [normed_group E] {f : α → E}
  {l : filter α} : is_o (1 : α → 𝕂) f l ↔ tendsto (λ x, ∥f x∥) l at_top :=
begin
  change is_o (λ _, 1 : α → 𝕂) f l ↔ _,
  refine ⟨λ h, _, λ h, _⟩,
  { rw (at_top_basis' (1 : ℝ)).tendsto_right_iff,
    intros c hc,
    have : 0 < c := zero_lt_one.trans_le hc,
    convert h.def (inv_pos.mpr this),
    ext x,
    rw [set.mem_Ici, norm_one, ← inv_mul_cancel (this.ne.symm),
        mul_le_mul_left (inv_pos.mpr this)] },
  { rw is_o_iff,
    intros c hc,
    filter_upwards [h.eventually (eventually_ge_at_top c⁻¹)],
    intros x hx,
    rwa [norm_one, ← mul_inv_cancel (hc.ne.symm), mul_le_mul_left hc] }
end

-- to mathlib
lemma asymptotics.is_O_with.eventually_eq_zero_imp {α 𝕂 : Type*} [normed_field 𝕂] {c : ℝ}
  {l : filter α} {f g : α → 𝕂} (h : is_O_with c f g l) : ∀ᶠ x in l, g x = 0 → f x = 0 :=
h.bound.mono (λ x hx hg, by simpa [hg] using hx)

-- to mathlib
lemma asymptotics.is_O.eventually_eq_zero_imp {α 𝕂 : Type*} [normed_field 𝕂]
  {l : filter α} {f g : α → 𝕂} (h : is_O f g l) : ∀ᶠ x in l, g x = 0 → f x = 0 :=
let ⟨c, hc⟩ := h.is_O_with in hc.eventually_eq_zero_imp

-- to mathlib
-- TODO : `tendsto f l at_top` is too strong, `∀ᶠ x in l, ∥f x - 1∥ ≥ ε` should be enough
lemma asymptotics.is_equivalent.left_comp_log_of_tendsto_at_top' {α : Type*} {f g : α → ℝ} {l : filter α}
  (h : f ~[l] g) (htop : tendsto g l at_top) : real.log ∘ f ~[l] real.log ∘ g :=
begin
  have hg : ∀ᶠ x in l, g x ≠ 0 := htop.eventually (eventually_ne_at_top 0),
  have hf : ∀ᶠ x in l, f x ≠ 0 := hg.mp (h.symm.is_O.eventually_eq_zero_imp.mono (λ x, mt)),
  have fact1 : is_o (real.log ∘ f - real.log ∘ g) (1 : α → ℝ) l,
  { refine (asymptotics.is_o_iff_tendsto (λ x (h : (1 : ℝ) = 0), (one_ne_zero h).elim)).2 _,
    simp only [function.comp_app, pi.one_apply, div_one, pi.sub_apply],
    have : tendsto (λ x, real.log (f x / g x)) l (𝓝 0) :=
      real.log_one ▸ ((is_equivalent_iff_tendsto_one hg).mp h).log one_ne_zero,
    refine this.congr' _,
    filter_upwards [hf, hg] (λ x hfx hgx, real.log_div hfx hgx) },
  have fact2 : is_o (1 : α → ℝ) (real.log ∘ g) l :=
    asymptotics.is_o_one_iff_left.mpr (tendsto_norm_at_top_at_top.comp $
      real.tendsto_log_at_top.comp htop),
  exact is_o.trans fact1 fact2
end

-- to mathlib
lemma asymptotics.is_equivalent.left_comp_log_of_tendsto_at_top {f g: ℝ → ℝ} {l: filter ℝ}
  (h: f ~[l] g) (htop: tendsto f l at_top): real.log ∘ f ~[l] real.log ∘ g :=
  asymptotics.is_equivalent.left_comp_log_of_tendsto_at_top' h (h.tendsto_at_top_iff.mp htop)

-- to mathlib
lemma asymptotics.is_o.congr_is_equivalent_left {u v w: ℝ → ℝ} {l: filter ℝ}
  (ho: is_o v w l) (h_equiv: u ~[l] v) : is_o u w l :=
begin
  convert is_o.add (is_o.trans h_equiv ho) ho,
  simp,
end

-- to mathlib
lemma real.is_o_id_exp_at_top : is_o id real.exp at_top :=
begin
  refine (asymptotics.is_o_iff_tendsto $ λ (x : ℝ) hx, (x.exp_pos.ne hx.symm).elim).mpr _,
  convert real.tendsto_div_pow_mul_exp_add_at_top 1 0 1 zero_ne_one (le_refl _),
  ext,
  simp
end

-- to mathlib
lemma real.is_o_log_id_at_top:
  is_o real.log id at_top :=
asymptotics.is_o.congr' (eventually_eq.refl _ _)
  ((eventually_gt_at_top 0).mono $ λ x hx, real.exp_log hx)
  (real.is_o_id_exp_at_top.comp_tendsto real.tendsto_log_at_top)

lemma tendsto_log1_plus_x_under_x_at_top_nhds_0 :
  tendsto (λ (x : ℝ), real.log (1 + x) / x) at_top (𝓝 0) :=
have this : 1 + id ~[at_top] id := (is_equivalent.refl).add_is_o
  (asymptotics.is_o_one_iff_left.mpr tendsto_norm_at_top_at_top),
(real.is_o_log_id_at_top.congr_is_equivalent_left $
  this.left_comp_log_of_tendsto_at_top' tendsto_id).tendsto_0

so beautiful

[Anatole Dedecker]

Oh and I forgot some easy generalizations, wait a second

[Ryan Lahfa]

I +1 the condition on left_comp_log_of_tendsto_at_top, it should be enough to say that f is eventually not approaching 1.

[Ryan Lahfa]

it should be cool to write down that log (1 + x) / x^n → 0 and log = o(x^n) in fact for any n ≥ 1 I think (?)

[Yaël Dillies]

for any n!

[Ryan Lahfa]

Yaël Dillies said:

for any n!

but $log x → +∞$ when $x → +∞$ ?!

[Anatole Dedecker]

Ryan Lahfa said:

it should be cool to write down that log (1 + x) / x^n → 0 and log = o(x^n) in fact for any n ≥ 1 I think (?)

Yes, it should be pretty easy to generalize to naturals ≥ 1. It should also be possible to generalize to reals > 0, though it may be a bit harder.

[Ryan Lahfa]

Anatole Dedecker said:

Ryan Lahfa said:

it should be cool to write down that log (1 + x) / x^n → 0 and log = o(x^n) in fact for any n ≥ 1 I think (?)

Yes, it should be pretty easy to generalize to naturals ≥ 1. It should also be possible to generalize to reals > 0, though it may be a bit harder.

The theorem for the limits already exist, but for reals > 0 do not I believe, so more generalization to do :>

[Anatole Dedecker]

I think Yaël might have thought that we are talking about $x\to 0$ ?

[Anatole Dedecker]

Ryan Lahfa said:

Anatole Dedecker said:

Ryan Lahfa said:

it should be cool to write down that log (1 + x) / x^n → 0 and log = o(x^n) in fact for any n ≥ 1 I think (?)

Yes, it should be pretty easy to generalize to naturals ≥ 1. It should also be possible to generalize to reals > 0, though it may be a bit harder.

The theorem for the limits already exist, but for reals > 0 do not I believe, so more generalization to do :>

Which theorem are you thinking about ? (the one that already exists)

[Ryan Lahfa]

Anatole Dedecker said:

Ryan Lahfa said:

Anatole Dedecker said:

Ryan Lahfa said:

it should be cool to write down that log (1 + x) / x^n → 0 and log = o(x^n) in fact for any n ≥ 1 I think (?)

Yes, it should be pretty easy to generalize to naturals ≥ 1. It should also be possible to generalize to reals > 0, though it may be a bit harder.

The theorem for the limits already exist, but for reals > 0 do not I believe, so more generalization to do :>

Which theorem are you thinking about ? (the one that already exists)

docs#real.tendsto_pow_mul_exp_neg_at_top_nhds_0

[Anatole Dedecker]

Oh yeah the exp one

[Anatole Dedecker]

Indeed I can't find it for rpow

[Anatole Dedecker]

Also, feel free to PR any part of my code if you want to take care of it.

[Ryan Lahfa]

It might be feasible to make it so that $\lim_{x \to +\infty} x^{\alpha} \exp(-\beta x) = 0$ with $\alpha, \beta > 0$ would be the general theorem, so we could have the generalization over reals with limits of form $\dfrac{\log^{\beta}(x)}{x^{\alpha}}$

[Ryan Lahfa]

Anatole Dedecker said:

Also, feel free to PR any part of my code if you want to take care of it.

If you prefer to do it, feel free, in all cases, I will try to PR some parts of my project (Ostrowski theorems) so it will be an arduous path, if I come around your parts and no PR is opened, or you do not have time, I am okay with shepherding it and doing the required changes :)

[Anatole Dedecker]

Ryan Lahfa said:

Anatole Dedecker said:

Also, feel free to PR any part of my code if you want to take care of it.

If you prefer to do it, feel free, in all cases, I will try to PR some parts of my project (Ostrowski theorems) so it will be an arduous path, if I come around your parts and no PR is opened, or you do not have time, I am okay with shepherding it and doing the required changes :)

I can do it, but I have other PRs to work on, so it might wait a little. If you're okay with that then I'll take care of the PR.

[Ryan Lahfa]

Anatole Dedecker said:

Ryan Lahfa said:

Anatole Dedecker said:

Also, feel free to PR any part of my code if you want to take care of it.

If you prefer to do it, feel free, in all cases, I will try to PR some parts of my project (Ostrowski theorems) so it will be an arduous path, if I come around your parts and no PR is opened, or you do not have time, I am okay with shepherding it and doing the required changes :)

I can do it, but I have other PRs to work on, so it might wait a little. If you're okay with that then I'll take care of the PR.

Definitely not in a hurry, thanks!