Zulip Chat Archive

Stream: Is there code for X?

Topic: Asymptotics conversions from equivalents


Ryan Lahfa (Aug 18 2021 at 15:04):

I'm looking at the asymptotics API to prove that log(1+x)/x0log(1+x)/x \to 0 when x+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 uvu \sim v, proving v=o(g)v = o(g) is equivalent to proving u=o(g)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 (Aug 18 2021 at 16:29):

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 (Aug 18 2021 at 16:49):

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 (Aug 18 2021 at 17:52):

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 (Aug 18 2021 at 18:45):

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 (Aug 18 2021 at 18:48):

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 (Aug 18 2021 at 18:48):

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 (Aug 18 2021 at 18:59):

Makes sense, then, thanks!

Anatole Dedecker (Aug 18 2021 at 19:37):

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 (Aug 18 2021 at 19:43):

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

Mario Carneiro (Aug 18 2021 at 19:45):

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 (Aug 18 2021 at 19:55):

Yes, I thought about this during dinner.

Anatole Dedecker (Aug 18 2021 at 23:03):

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 (Aug 18 2021 at 23:07):

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 (Aug 18 2021 at 23:08):

Oh and I forgot some easy generalizations, wait a second

Ryan Lahfa (Aug 18 2021 at 23:08):

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 (Aug 18 2021 at 23:09):

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 (Aug 18 2021 at 23:17):

for any n!

Ryan Lahfa (Aug 18 2021 at 23:24):

Yaël Dillies said:

for any n!

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

Anatole Dedecker (Aug 18 2021 at 23:24):

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 (Aug 18 2021 at 23:24):

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 (Aug 18 2021 at 23:26):

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

Anatole Dedecker (Aug 18 2021 at 23:29):

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 (Aug 18 2021 at 23:30):

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 (Aug 18 2021 at 23:32):

Oh yeah the exp one

Anatole Dedecker (Aug 18 2021 at 23:35):

Indeed I can't find it for rpow

Anatole Dedecker (Aug 18 2021 at 23:36):

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

Ryan Lahfa (Aug 18 2021 at 23:36):

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

Ryan Lahfa (Aug 18 2021 at 23:37):

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 (Aug 18 2021 at 23:44):

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 (Aug 18 2021 at 23:49):

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!


Last updated: Dec 20 2023 at 11:08 UTC